suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Fixed issue with type-infer, application case

Browse Source 
Application case was expecting type-infer to return a normal form.
This cannot be expected.
This commit is contained in:
William J. Bowman 2016-01-08 19:44:40 -05:00
parent 86a2e0d2ed
commit cfa81e3508
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 7 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
curnel/redex-core.rkt
View File

@ -877,7 +877,9 @@
----------------- "DTR-Product"
(type-infer Δ Γ (Π (x : t_0) t) U)]
[(type-infer Δ Γ e_0 (Π (x_0 : t_0) t_1))
[(type-infer Δ Γ e_0 t)
;; Cannot rely on type-infer producing normal forms.
(where (Π (x_0 : t_0) t_1) (reduce Δ t))
(type-check Δ Γ e_1 t_0)
(where t_3 (subst t_1 x_0 e_1))
----------------- "DTR-Application"
@ -1186,6 +1188,10 @@
,zero?)
(λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
,ih-equal?)))))
(check-holds
(type-check ,Δ (∅ nat-equal? : (Π (x-D«4158» : nat) ((λ (x«4159» : nat) (Π (x«4160» : nat) bool)) x-D«4158»)))
((nat-equal? zero) zero)
bool))
(check-holds
(type-check ,Δ ∅
,nat-equal?