From 87f8ae99ebf83245dcfeee38bb2c4ccb93b47121 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 14 Mar 2020 15:07:14 -0700 Subject: [PATCH] test: `reduceBool` test --- tests/lean/run/kernel1.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/kernel1.lean b/tests/lean/run/kernel1.lean index 608b27ad1f..0668140064 100644 --- a/tests/lean/run/kernel1.lean +++ b/tests/lean/run/kernel1.lean @@ -34,4 +34,4 @@ def c5 := reduceNat v5 #eval checkDefEq `c5 `Nat.zero #eval checkDefEq `Nat.zero `c5 --- #eval checkDefEq `c4 `Bool.true -- It crashes due to a bug at run_boxed +#eval checkDefEq `c4 `Bool.true