git.iko.soy/Idris-dev
on master help sign in
Really replaced `lteZero` with `LTEZero`
3867dbaAhmad Salim Al-Sibahi
test/totality006/totality006.idr+1−1
compare with master
unifiedsplit
@@ -5,7 +5,7 @@ total
5prf : (a:Nat) -> (b:Nat) -> So (a > b) -> GT a b
5prf : (a:Nat) -> (b:Nat) -> So (a > b) -> GT a b
6prf Z Z Oh impossible
6prf Z Z Oh impossible
7prf Z (S k) um = antitrue um
7prf Z (S k) um = antitrue um
8−prf (S k) Z um = LTESucc lteZero
8+prf (S k) Z um = LTESucc LTEZero
9-- prf (S _) (S _) Oh impossible
9-- prf (S _) (S _) Oh impossible
10
10
11
11
test/totality006/totality006a.idr+1−1
@@ -5,6 +5,6 @@ total
5prf' : (a:Nat) -> (b:Nat) -> So (a > b) -> GT a b
5prf' : (a:Nat) -> (b:Nat) -> So (a > b) -> GT a b
6prf' Z Z Oh impossible
6prf' Z Z Oh impossible
7prf' Z (S k) um = antitrue um
7prf' Z (S k) um = antitrue um
8−prf' (S k) Z um = LTESucc lteZero
8+prf' (S k) Z um = LTESucc LTEZero
9prf' (S _) (S _) Oh impossible
9prf' (S _) (S _) Oh impossible
10
10