lib: use a debugger to step into the compiler to figure out how the b…

…ug appears and fix it by rewriting the code
aya-prover · Feb 13, 2023 · 4b6fff2 · 4b6fff2
1 parent 1e071c6
commit 4b6fff2
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/base/src/test/resources/success/common/src/Arith/Nat/Order.aya b/base/src/test/resources/success/common/src/Arith/Nat/Order.aya
@@ -1,4 +1,5 @@
 open import Arith::Nat::Core
+open import Arith::Nat::Properties
 open import Logic::False
 open import Logic::Dec
 open import Paths

diff --git a/base/src/test/resources/success/common/src/Logic/HLevels.aya b/base/src/test/resources/success/common/src/Logic/HLevels.aya
@@ -9,4 +9,4 @@ open import Arith::Nat::Core
 def isHLvl Nat Type : Type
 | 0, A => isContr A
 | 1, A => isProp A
-| suc n, A => ∀ a b -> isHLvl n (a = b)
+| suc n, A => ∀ (a b : A) -> isHLvl n (a = b)