Fix typechecking

JetBrains · Oct 9, 2020 · 2d7b69c · 2d7b69c
1 parent ca51158
commit 2d7b69c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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 (<=)