diff options
Diffstat (limited to 'stlc-ext.rkt')
| -rw-r--r-- | stlc-ext.rkt | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/stlc-ext.rkt b/stlc-ext.rkt index 300a473..84c476c 100644 --- a/stlc-ext.rkt +++ b/stlc-ext.rkt @@ -1,5 +1,6 @@ #lang racket (require "lib.rkt") +(require "base.rkt") (provide interpret check infer expand equiv-type equiv-term) ;; The Simply-Typed Lambda Calculus, with simple extensions @@ -252,13 +253,3 @@ [(`(,l1 ...) `(,l2 ...)) (foldl (λ (x1 x2 acc) (if (equiv-term-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] [(v1 v2) (equal? v1 v2)])) - -(require rackunit) -(define-test-suite ext - (check-true (equiv-term '(λ a a) '(λ b b) #hash())) - (check-true (equiv-term '(λ a (λ b a)) '(λ b (λ a b)) #hash())) - (check-true (equiv-term '(λ a (λ b (λ c (a (b c))))) '(λ c (λ a (λ b (c (a b))))) #hash())) - (check-eq? (interpret '(if #t 1 0)) 1) - (check-eq? (interpret '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 2) - (check-eq? (infer '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 'Nat) - (check-true (check '(type Natural Nat ((λ (x : Natural) (inc x)) 1)) 'Nat))) |