git.iko.soy/Idris-dev
on 5e2000e help sign in
Idris-dev/test/proof009/expected
26 lines 833 B history raw
1Warning: this interactive prover is deprecated and will be removed in a future release. Please see :elab for a similar feature that will replace it.
4---------- Goal: ----------
5{hole_0} : Int -> Int -> Int
6-Main.arhs> ---------- Other goals: ----------
7{hole_0}
8---------- Assumptions: ----------
9 x : Int
10---------- Goal: ----------
11{hole_1} : Int -> Int
12-Main.arhs> ---------- Other goals: ----------
13{hole_1},{hole_0}
14---------- Assumptions: ----------
15 x : Int
16 y : Int
17---------- Goal: ----------
18{hole_2} : Int
19-Main.arhs> arhs: No more goals.
20-Main.arhs> Proof completed!
21Main.arhs = proof
22 intro x
23 intros
24 trivial