git.iko.soy/Idris-dev
on master help sign in
suc{Max,Min}{L,R} + add mrb to CONTRIBUTORS
dfa272dmrb
CONTRIBUTORS+1
compare with master
unifiedsplit
@@ -4,6 +4,7 @@ Ozgur Akgun
4Ahmad Salim Al-Sibahi
4Ahmad Salim Al-Sibahi
5Edward Chadwick Amsden
5Edward Chadwick Amsden
6Jan Bessai
6Jan Bessai
7+Michael R. Bernstein
7Nicola Botta
8Nicola Botta
8Edwin Brady
9Edwin Brady
9David Raymond Christiansen
10David Raymond Christiansen
libs/prelude/Prelude/Nat.idr+16
@@ -697,6 +697,22 @@ maximumSuccSucc (S left) (S right) =
697 let inductiveHypothesis = maximumSuccSucc left right in
697 let inductiveHypothesis = maximumSuccSucc left right in
698 ?maximumSuccSuccStepCase
698 ?maximumSuccSuccStepCase
699
699
700+total sucMaxL : (l : Nat) -> maximum (S l) l = (S l)
701+sucMaxL Z = refl
702+sucMaxL (S l) = cong (sucMaxL l)
703+
704+total sucMaxR : (l : Nat) -> maximum l (S l) = (S l)
705+sucMaxR Z = refl
706+sucMaxR (S l) = cong (sucMaxR l)
707+
708+total sucMinL : (l : Nat) -> minimum (S l) l = l
709+sucMinL Z = refl
710+sucMinL (S l) = cong (sucMinL l)
711+
712+total sucMinR : (l : Nat) -> minimum l (S l) = l
713+sucMinR Z = refl
714+sucMinR (S l) = cong (sucMinR l)
715+
700-- div and mod
716-- div and mod
701total modZeroZero : (n : Nat) -> mod 0 n = Z
717total modZeroZero : (n : Nat) -> mod 0 n = Z
702modZeroZero Z = refl
718modZeroZero Z = refl