diff --git a/Algo.hs b/Algo.hs index d153061..e460c71 100644 --- a/Algo.hs +++ b/Algo.hs @@ -197,5 +197,8 @@ test1 = typecheck (Abs "A" (Abs "x" (Var "x"))) (Pi "A" Type (Pi "x" (Var "A") (Var "A"))) test2 :: Result -test2 = typecheck (Abs "A" (Abs "f" (Abs "x" (App (Var "f") (Var "x"))))) - (Pi "A" Type (Pi "f" (Pi "_" (Var "A") (Var "A")) (Pi "x" (Var "A") (Var "A")))) +test2 = typecheck (Abs "A" (Abs "B" (Abs "f" (Abs "x" (App (Var "f") (Var "x")))))) + (Pi "A" Type + (Pi "B" (Pi "_" (Var "A") Type) + (Pi "f" (Pi "a" (Var "A") (App (Var "B") (Var "a"))) + (Pi "x" (Var "A") (App (Var "B") (Var "x"))))))