@@ -1,12 +1,38 @@
5+-- An expensive function.
3qib : Nat -> Nat
6qib : Nat -> Nat
5−qib (S Z) = 1
8+qib (S Z) = 2
6qib (S (S n)) = qib n * qib (S n)
9qib (S (S n)) = qib n * qib (S n)
11+-- An equality whose size reflects the size of numbers.
12+data equals : Nat -> Nat -> Type where
14+ eqS : m `equals` n -> S m `equals` S n
16+eq_refl : {n : Nat} -> n `equals` n
18+eq_refl {n = S n} = eqS eq_refl
20+-- Here, the proof is very expensive to compute.
21+-- We add a recursive argument to prevent Idris from inlining it.
22+f : (r, n : Nat) -> Subset Nat (\k => qib n `equals` qib k)
23+f Z n = element n eq_refl
26+-- Here, the witness is very expensive to compute.
27+-- We add a recursive argument to prevent Idris from inlining it.
8−f : (n : Nat) -> Exists (\k : Nat => qib n = k)
28+g : (r, n : Nat) -> Exists (\k : Nat => k = qib n)
9−f n = evidence (qib n) refl
29+g Z n = evidence (qib n) refl
33+nod _ = putStrLn "*nod*"
11main : IO ()
35main : IO ()
12−main = print "hello world"
36+main = do
37+ nod $ getWitness (f 4 2)
38+ nod $ getProof (g 4 2)