Add pi types

2025-05-12 16:28:54 -04:00 · 2025-05-12 16:28:54 -04:00 · f418c383f3
commit f418c383f3
parent da9ea4ed93
3 changed files with 23 additions and 5 deletions
--- a/nbe-test.rkt
+++ b/nbe-test.rkt
@ -97,4 +97,5 @@
              (tm-pnat 12000))
 (check βη-eq? (tm-padd (tm-pnat 10000) (tm-pnat 2000)) (tm-pnat 12000))
 (check βη-eq? (tm-abs (tm-app (tm-var 1) (tm-var 0))) (tm-app tm-id (tm-var 0)))
+(check βη-eq? `(Π (U 0) (Π (var 0) ,(tm-app tm-id '(var 1)))) '(Π (U 0) (Π (var 0) (var 1))))
 (check-false (βη-eq? '(U 0) '(var 0)))