diff options
author | JJ | 2024-07-27 00:14:26 +0000 |
---|---|---|
committer | JJ | 2024-07-27 00:14:26 +0000 |
commit | c9651d9c20c94e2fb45b5ac4ec3bb350dc2dfd4b (patch) | |
tree | 5af74a33f9198871d73bf9bf4b22d3028d3e8dcc /stlc-rec.rkt | |
parent | 062686cb4394512f337020f79eb16ac232ba9788 (diff) |
backport check case reduction
Diffstat (limited to 'stlc-rec.rkt')
-rw-r--r-- | stlc-rec.rkt | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/stlc-rec.rkt b/stlc-rec.rkt index c90fdae..342f265 100644 --- a/stlc-rec.rkt +++ b/stlc-rec.rkt @@ -41,11 +41,6 @@ (check-core (desugar expr) with #hash())) (define (check-core expr with Γ) (match expr - ['sole (equal? 'Unit with)] - [n #:when (natural? n) (equal? 'Nat with)] - [x #:when (dict-has-key? Γ x) - (equal? (dict-ref Γ x) with)] - [`(fold (μ ,x ,t) ,e) (match with [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))] @@ -56,11 +51,6 @@ [`(,t1 → ,t2) (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))] [_ #f])] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,t2) - (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))] - [_ #f])] [_ (equal? (infer-core expr Γ) with)])) |