git.iko.soy/Idris-dev
on 5570cee help sign in
Idris-dev/tutorial/examples/theorems.idr
38 lines 704 B history raw
2fiveIsFive : 5 = 5
3fiveIsFive = refl
5twoPlusTwo : 2 + 2 = 4
6twoPlusTwo = refl
8plusReduces : (n:Nat) -> plus O n = n
9plusReduces n = refl
11plusReducesO : (n:Nat) -> n = plus n O
12plusReducesO O = refl
13plusReducesO (S k) = eqRespS (plusReducesO k)
15plusReducesS : (n:Nat) -> (m:Nat) -> S (plus n m) = plus n (S m)
16plusReducesS O m = refl
17plusReducesS (S k) m = eqRespS (plusReducesS k m)
19plusReducesO' : (n:Nat) -> n = plus n O
20plusReducesO' O = ?plusredO_O
21plusReducesO' (S k) = let ih = plusReducesO' k in
22 ?plusredO_S
25---------- Proofs ----------
27plusredO_S = proof {
28 intro;
29 intro;
30 rewrite ih;
31 trivial;
34plusredO_O = proof {
35 compute;
36 trivial;