From 0b0a2eed406062f91420659e15b8e56c781c7beb Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 25 Mar 2016 02:57:22 -0400 Subject: [PATCH] Added some missing wf checks --- cur-lib/cur/curnel/redex-core.rkt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/cur-lib/cur/curnel/redex-core.rkt b/cur-lib/cur/curnel/redex-core.rkt index ff31503..9892ffe 100644 --- a/cur-lib/cur/curnel/redex-core.rkt +++ b/cur-lib/cur/curnel/redex-core.rkt @@ -494,16 +494,19 @@ [(side-condition (Δ-in-dom Δ x)) (where t (Δ-ref-type Δ x)) + (wf Δ Γ) ----------------- "DTR-Inductive" (type-infer Δ Γ x t)] [(side-condition (Δ-in-constructor-dom Δ x)) (where t (Δ-ref-constructor-type Δ x)) + (wf Δ Γ) ----------------- "DTR-Constructor" (type-infer Δ Γ x t)] [(side-condition (Γ-in-dom Γ x)) (where t (Γ-ref Γ x)) + (wf Δ Γ) ----------------- "DTR-Start" (type-infer Δ Γ x t)]