Really replaced `lteZero` with `LTEZero`
commit3867dba4eceb15b7335ecfb6ab2c91018f83462b
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateFri 26 Sep 2014, 18:38 (12 years ago)
parent562da7b
test/totality006/totality006.idr+1−1
@@ -5,7 +5,7 @@ total
55prf : (a:Nat) -> (b:Nat) -> So (a > b) -> GT a b
66prf Z Z Oh impossible
77prf Z (S k) um = antitrue um
8−prf (S k) Z um = LTESucc lteZero
8+prf (S k) Z um = LTESucc LTEZero
99-- prf (S _) (S _) Oh impossible
1010
1111
test/totality006/totality006a.idr+1−1
@@ -5,6 +5,6 @@ total
55prf' : (a:Nat) -> (b:Nat) -> So (a > b) -> GT a b
66prf' Z Z Oh impossible
77prf' Z (S k) um = antitrue um
8−prf' (S k) Z um = LTESucc lteZero
8+prf' (S k) Z um = LTESucc LTEZero
99prf' (S _) (S _) Oh impossible
1010