From 2d7b69c64f9ae7ba35d2358d73e487f6646e0554 Mon Sep 17 00:00:00 2001
From: valis <valery.isaev@gmail.com>
Date: Fri, 9 Oct 2020 21:13:04 +0300
Subject: [PATCH] Fix typechecking

---
 src/Arith/Nat.ard | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Arith/Nat.ard b/src/Arith/Nat.ard
index 1bdb5f43..7ede7f9d 100644
--- a/src/Arith/Nat.ard
+++ b/src/Arith/Nat.ard
@@ -158,4 +158,4 @@
     | suc (suc k), q => <=_+ (<=-transitive <=-suc (<_*_positive-left p (suc<=suc zero<=_))) p
   }
   | <_*_negative-left x<y z<0 => \case z<0 \with {}
-  \where \open LinearOrder
+  \where \open LinearOrder \hiding (<=)