resolve: more tests

aya-prover · Jan 6, 2025 · 1171a97 · 1171a97
1 parent 594c2af
commit 1171a97
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java
@@ -177,9 +177,12 @@ public void testVariableDefinition() {
       open inductive K | kk
       open inductive G (k : K) | gg
       open inductive F (A : Type) (k : K) (n : G k) | ff
+      open inductive N (b : A) (c : A) | nn
       variable k : K
       variable n : G k
       variable xs : F A k n
+      variable b c : A
+      variable d : N b c
       def infix = (a b : A) => Path (\\i => A) a b
     """).defs;
     assertTrue(result.isNotEmpty());