resolve: more test for dependent types in variable

aya-prover · Dec 23, 2024 · 6473239 · 6473239
1 parent 7c9b885
commit 6473239
Showing 1 changed file with 6 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,6 +177,12 @@ public void testVariableDefinition() {
       prim I prim Path
       variable A : Type
       variable a : A
+      open inductive K | kk
+      open inductive G (k : K) | gg
+      open inductive F (A : Type) (k : K) (n : G k) | ff
+      variable k : K
+      variable n : G k
+      variable xs : F A k n
       def infix = (a b : A) => Path (\\i => A) a b
     """).defs;
     assertTrue(result.isNotEmpty());