From 8eaedabe3b0b576c7bdb8d7c1bc1cdf240e5203b Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 8 Jan 2016 20:06:00 -0500 Subject: [PATCH] =?UTF-8?q?Fixed=20broken=20test=20caused=20by=20fix=20to?= =?UTF-8?q?=20=CE=A0=20dyn.=20sem.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- curnel/redex-core.rkt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/curnel/redex-core.rkt b/curnel/redex-core.rkt index c500d47..61ec66b 100644 --- a/curnel/redex-core.rkt +++ b/curnel/redex-core.rkt @@ -620,7 +620,7 @@ (check-not-equiv? (term (reduce ∅ ((Π (x : t) x) (Unv 0)))) (term (Unv 0))) (check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) x_0) (Unv 0))))) (term (Π (x : t) (Unv 0)))) - (check-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x)))) + (check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x)))) (term (Π (x : t) (x x)))) (check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat)) (s zero))