Test about Pi and Sigma (#147)

JetBrains · Apr 13, 2020 · 1a67207 · 1a67207
1 parent 7af86f3
commit 1a67207
Showing 1 changed file with 16 additions and 3 deletions.
diff --git a/src/test/java/org/arend/typechecking/AppHoleTest.java b/src/test/java/org/arend/typechecking/AppHoleTest.java
@@ -49,6 +49,18 @@ public void inLam() {
     checkAsLam("Nat -> Nat -> Nat", "\\lam x => __ Nat.+ x");
   }
 
+  @Test
+  public void inPi() {
+    checkAsLam("Nat -> \\Set0", "\\Pi (A : 1 = __) -> Nat");
+    checkAsLam("\\Set0 -> \\Set1", "\\Pi (A : __) -> Nat");
+  }
+
+  @Test
+  public void inSigma() {
+    checkAsLam("Nat -> \\Set0", "\\Sigma (A : 1 = __) Nat");
+    checkAsLam("\\Set0 -> \\Set1", "\\Sigma (A : __) Nat");
+  }
+
   @Test
   public void inCase() {
     checkAsLam("Nat -> Nat -> Nat",
@@ -64,13 +76,14 @@ public void inBinOpWithProj() {
 
   @Test
   public void inTuple() {
-    Expression ty = typeCheckExpr("(\\Sigma ((\\Sigma Nat Nat) -> Nat) ((\\Sigma Nat Nat) -> Nat))", null).expression;
+    Expression ty = typeCheckExpr(
+        "(\\Sigma ((\\Sigma Nat Nat) -> Nat) ((\\Sigma Nat Nat) -> Nat))", null).expression;
     Expression result = typeCheckExpr("(__.1, __.2)", ty).expression;
     assertTrue(result instanceof TupleExpression);
     TupleExpression tuple = (TupleExpression) result;
     assertEquals(2, tuple.getFields().size());
-    assertTrue(tuple.getFields().get(0) instanceof LamExpression);
-    assertTrue(tuple.getFields().get(1) instanceof LamExpression);
+    for (Expression field : tuple.getFields())
+      assertTrue(field instanceof LamExpression);
   }
 
   @Test