rachel
/
an-algorithm-for-checking-dependent-types
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

include application test

master
Rachel Lambda Samuelsson 2022-05-12 19:01:19 +02:00
parent d701a81172
commit cb00846b94
1 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
Algo.hs
View File

@ -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"))))))