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

where #t is stupid; use side-condition

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

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

@ -492,17 +492,17 @@
----------------- "DTR-Unv" ----------------- "DTR-Unv"
(type-infer Δ Γ U_0 U_1)] (type-infer Δ Γ U_0 U_1)]
[(where #t (Δ-in-dom Δ x)) [(side-condition (Δ-in-dom Δ x))
(where t (Δ-ref-type Δ x)) (where t (Δ-ref-type Δ x))
----------------- "DTR-Inductive" ----------------- "DTR-Inductive"
(type-infer Δ Γ x t)] (type-infer Δ Γ x t)]
[(where #t (Δ-in-constructor-dom Δ x)) [(side-condition (Δ-in-constructor-dom Δ x))
(where t (Δ-ref-constructor-type Δ x)) (where t (Δ-ref-constructor-type Δ x))
----------------- "DTR-Constructor" ----------------- "DTR-Constructor"
(type-infer Δ Γ x t)] (type-infer Δ Γ x t)]
[(where #t (Γ-in-dom Γ x)) [(side-condition (Γ-in-dom Γ x))
(where t (Γ-ref Γ x)) (where t (Γ-ref Γ x))
----------------- "DTR-Start" ----------------- "DTR-Start"
(type-infer Δ Γ x t)] (type-infer Δ Γ x t)]