Renamed 'lteSucc' and 'lteZero' in tests to 'LTESucc' and 'LTEZero'
commit562da7b7e685e485176c352a09083ed1a6c06d0c
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateFri 26 Sep 2014, 18:09 (12 years ago)
parent5a257a4
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