@@ -0,0 +1,43 @@
1+module Main
2+
3+%default total
4+
5+-- An expensive function.
6+qib : Nat -> Nat
7+qib Z = 1
8+qib (S Z) = 2
9+qib (S (S n)) = qib n * qib (S n)
10+
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 the function.
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+-- A (contrived) relation, just to have something to show.
27+data represents : Nat -> Nat -> Type where
28+ axiom : (n : Nat) -> qib n `represents` n
29+
30+-- Here, the witness is very expensive to compute.
31+-- We add a recursive argument to prevent Idris from inlining the function.
32+g : (r, n : Nat) -> Exists (\k : Nat => k `represents` n)
33+g Z n = evidence (qib n) (axiom n)
34+g (S r) n = g r n
35+
36+fmt : qib n `represents` n -> String
37+fmt (axiom n) = "axiom " ++ show n
38+
39+main : IO ()
40+main = do
41+ n <- map (const 10000) (putStrLn "*oink*")
42+ putStrLn . show $ getWitness (f 4 n)
43+ putStrLn . fmt $ getProof (g 4 n)