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

Fixed bug in well-formed inductive type checker

Browse Source
This commit is contained in:
William J. Bowman 2016-03-25 00:50:24 -04:00
parent 543a7f93e6
commit 816da683ec
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
cur-lib/cur/curnel/redex-core.rkt
View File

@ -476,7 +476,7 @@
(type-infer Δ ∅ t_D U_D) (type-infer Δ ∅ t_D U_D)
(type-infer Δ (∅ D : t_D) t_c U_c) ... (type-infer Δ (∅ D : t_D) t_c U_c) ...
;; NB: Ugh this should be possible with pattern matching alone .... ;; NB: Ugh this should be possible with pattern matching alone ....
(side-condition ,(map (curry equal? (term D)) (term (D_0 ...)))) (side-condition ,(andmap (curry equal? (term D)) (term (D_0 ...))))
(side-condition (positive* D (t_c ...))) (side-condition (positive* D (t_c ...)))
----------------- "WF-Inductive" ----------------- "WF-Inductive"
(wf (Δ (D : t_D (wf (Δ (D : t_D