@@ -1,12 +1,38 @@
11module Main
22
3+%default total
4+
5+-- An expensive function.
36qib : Nat -> Nat
4−qib Z = 1
5−qib (S Z) = 1
7+qib Z = 2
8+qib (S Z) = 2
69qib (S (S n)) = qib n * qib (S n)
710
8−f : (n : Nat) -> Exists (\k : Nat => qib n = k)
9−f n = evidence (qib n) refl
11+-- An equality whose size reflects the size of numbers.
12+data equals : Nat -> Nat -> Type where
13+ eqZ : Z `equals` Z
14+ eqS : m `equals` n -> S m `equals` S n
15+
16+eq_refl : {n : Nat} -> n `equals` n
17+eq_refl {n = Z} = eqZ
18+eq_refl {n = S n} = eqS eq_refl
19+
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
24+f (S r) n = f r n
25+
26+-- Here, the witness is very expensive to compute.
27+-- We add a recursive argument to prevent Idris from inlining it.
28+g : (r, n : Nat) -> Exists (\k : Nat => k = qib n)
29+g Z n = evidence (qib n) refl
30+g (S r) n = g r n
31+
32+nod : a -> IO ()
33+nod _ = putStrLn "*nod*"
1034
1135main : IO ()
12−main = print "hello world"
36+main = do
37+ nod $ getWitness (f 4 2)
38+ nod $ getProof (g 4 2)