@@ -4,7 +4,7 @@ module Main
44
55-- An expensive function.
66qib : Nat -> Nat
7−qib Z = 2
7+qib Z = 1
88qib (S Z) = 2
99qib (S (S n)) = qib n * qib (S n)
1010
@@ -18,21 +18,26 @@ eq_refl {n = Z} = eqZ
1818eq_refl {n = S n} = eqS eq_refl
1919
2020-- Here, the proof is very expensive to compute.
21−-- We add a recursive argument to prevent Idris from inlining it.
21+-- We add a recursive argument to prevent Idris from inlining the function.
2222f : (r, n : Nat) -> Subset Nat (\k => qib n `equals` qib k)
2323f Z n = element n eq_refl
2424f (S r) n = f r n
2525
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+
2630-- 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
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)
3034g (S r) n = g r n
3135
32−nod : a -> IO ()
33−nod _ = putStrLn "*nod*"
36+fmt : qib n `represents` n -> String
37+fmt (axiom n) = "axiom " ++ show n
3438
3539main : IO ()
3640main = do
37− nod $ getWitness (f 4 2)
38− nod $ getProof (g 4 2)
41+ n <- map (const 10000) (putStrLn "*oink*")
42+ putStrLn . show $ getWitness (f 4 n)
43+ putStrLn . fmt $ getProof (g 4 n)