git.iko.soy/Idris-dev
on 372d2ea help sign in
Idris-dev/test/proof009/expected
26 lines 827 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{hole0} : Int -> Int -> Int
6-Main.arhs> ---------- Other goals: ----------
7{hole0}
8---------- Assumptions: ----------
9 x : Int
10---------- Goal: ----------
11{hole1} : Int -> Int
12-Main.arhs> ---------- Other goals: ----------
13{hole1},{hole0}
14---------- Assumptions: ----------
15 x : Int
16 y : Int
17---------- Goal: ----------
18{hole2} : Int
19-Main.arhs> arhs: No more goals.
20-Main.arhs> Proof completed!
21Main.arhs = proof
22 intro x
23 intros
24 trivial