diff options
Diffstat (limited to 'stlc-let.rkt')
| -rw-r--r-- | stlc-let.rkt | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/stlc-let.rkt b/stlc-let.rkt index 04dbd84..edf39a7 100644 --- a/stlc-let.rkt +++ b/stlc-let.rkt @@ -27,11 +27,11 @@ [(n 'Nat) #:when (natural? n) #t] [(x _) #:when (dict-has-key? Γ x) (equal? (dict-ref Γ x) with)] - [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2)) + [(`(λ (,x : ,t) ,e) `(,t1 → ,t2)) (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) (match (infer- e1 Γ) - [`(→ ,t1 ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] + [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] [t #f])] [(e t) #f])) @@ -42,11 +42,11 @@ (match expr ['sole 'Unit] [n #:when (natural? n) 'Nat] - [`(λ ,x (: ,t) ,e) - `(→ ,t ,(infer- e (dict-set Γ x t)))] + [`(λ (,x : ,t) ,e) + `(,t → ,(infer- e (dict-set Γ x t)))] [`(,e1 ,e2) (match (infer- e1 Γ) - [`(→ ,t1 ,t2) + [`(,t1 → ,t2) (if (check- e2 t1 Γ) t2 (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))] [t (err (format "expected → type on application body, got ~a" t))])] |