git.iko.soy/Idris-dev
on master help sign in
Renamed 'lteSucc' and 'lteZero' in tests to 'LTESucc' and 'LTEZero'
562da7bAhmad 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