From 816da683ec005ff567ef9e6b488264cdf7104a40 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 25 Mar 2016 00:50:24 -0400 Subject: [PATCH] Fixed bug in well-formed inductive type checker --- cur-lib/cur/curnel/redex-core.rkt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cur-lib/cur/curnel/redex-core.rkt b/cur-lib/cur/curnel/redex-core.rkt index 10f31f1..ad4b4ea 100644 --- a/cur-lib/cur/curnel/redex-core.rkt +++ b/cur-lib/cur/curnel/redex-core.rkt @@ -476,7 +476,7 @@ (type-infer Δ ∅ t_D U_D) (type-infer Δ (∅ D : t_D) t_c U_c) ... ;; 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 ...))) ----------------- "WF-Inductive" (wf (Δ (D : t_D