git.iko.soy/Idris-dev
on 239c8ca help sign in
Idris-dev/test/proof009/expected
25 lines 678 B history raw
3---------- Goal: ----------
4{hole0} : Int -> Int -> Int
5-Main.arhs> ---------- Other goals: ----------
6{hole0}
7---------- Assumptions: ----------
8 x : Int
9---------- Goal: ----------
10{hole1} : Int -> Int
11-Main.arhs> ---------- Other goals: ----------
12{hole1},{hole0}
13---------- Assumptions: ----------
14 x : Int
15 y : Int
16---------- Goal: ----------
17{hole2} : Int
18-Main.arhs> arhs: No more goals.
19-Main.arhs> Proof completed!
20Main.arhs = proof
21 intro x
22 intros
23 trivial