From cb00846b940b8c00ecd29839c45a179fb2c21b1b Mon Sep 17 00:00:00 2001 From: depsterr Date: Thu, 12 May 2022 19:01:19 +0200 Subject: [PATCH] include application test --- Algo.hs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) 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"))))))