Really replaced lteZero with LTEZero

idris-lang · Sep 26, 2014 · 3867dba · 3867dba
1 parent 562da7b
commit 3867dba
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/test/totality006/totality006.idr b/test/totality006/totality006.idr
@@ -5,7 +5,7 @@ total
 prf : (a:Nat) -> (b:Nat) -> So (a > b) -> GT a b
 prf Z     Z     Oh impossible
 prf Z     (S k) um = antitrue um
-prf (S k) Z     um = LTESucc lteZero 
+prf (S k) Z     um = LTESucc LTEZero 
 -- prf (S _) (S _) Oh impossible
 
 
diff --git a/test/totality006/totality006a.idr b/test/totality006/totality006a.idr
@@ -5,6 +5,6 @@ total
 prf' : (a:Nat) -> (b:Nat) -> So (a > b) -> GT a b
 prf' Z     Z     Oh impossible
 prf' Z     (S k) um = antitrue um
-prf' (S k) Z     um = LTESucc lteZero 
+prf' (S k) Z     um = LTESucc LTEZero 
 prf' (S _) (S _) Oh impossible