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

Added some missing wf checks

Browse Source
This commit is contained in:
William J. Bowman 2016-03-25 02:57:22 -04:00
parent 64c8edfde4
commit 0b0a2eed40
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -494,16 +494,19 @@
[(side-condition (Δ-in-dom Δ x)) [(side-condition (Δ-in-dom Δ x))
(where t (Δ-ref-type Δ x)) (where t (Δ-ref-type Δ x))
(wf Δ Γ)
----------------- "DTR-Inductive" ----------------- "DTR-Inductive"
(type-infer Δ Γ x t)] (type-infer Δ Γ x t)]
[(side-condition (Δ-in-constructor-dom Δ x)) [(side-condition (Δ-in-constructor-dom Δ x))
(where t (Δ-ref-constructor-type Δ x)) (where t (Δ-ref-constructor-type Δ x))
(wf Δ Γ)
----------------- "DTR-Constructor" ----------------- "DTR-Constructor"
(type-infer Δ Γ x t)] (type-infer Δ Γ x t)]
[(side-condition (Γ-in-dom Γ x)) [(side-condition (Γ-in-dom Γ x))
(where t (Γ-ref Γ x)) (where t (Γ-ref Γ x))
(wf Δ Γ)
----------------- "DTR-Start" ----------------- "DTR-Start"
(type-infer Δ Γ x t)] (type-infer Δ Γ x t)]