From 64c8edfde4d62a60d9a48c3d3af278449b6a55c5 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 25 Mar 2016 02:55:45 -0400 Subject: [PATCH] where #t is stupid; use side-condition --- cur-lib/cur/curnel/redex-core.rkt | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/cur-lib/cur/curnel/redex-core.rkt b/cur-lib/cur/curnel/redex-core.rkt index 4d5cb21..ff31503 100644 --- a/cur-lib/cur/curnel/redex-core.rkt +++ b/cur-lib/cur/curnel/redex-core.rkt @@ -492,17 +492,17 @@ ----------------- "DTR-Unv" (type-infer Δ Γ U_0 U_1)] - [(where #t (Δ-in-dom Δ x)) + [(side-condition (Δ-in-dom Δ x)) (where t (Δ-ref-type Δ x)) ----------------- "DTR-Inductive" (type-infer Δ Γ x t)] - [(where #t (Δ-in-constructor-dom Δ x)) + [(side-condition (Δ-in-constructor-dom Δ x)) (where t (Δ-ref-constructor-type Δ x)) ----------------- "DTR-Constructor" (type-infer Δ Γ x t)] - [(where #t (Γ-in-dom Γ x)) + [(side-condition (Γ-in-dom Γ x)) (where t (Γ-ref Γ x)) ----------------- "DTR-Start" (type-infer Δ Γ x t)]