diff --git a/tests/lean/simp32.lean b/tests/lean/simp32.lean index 50d68b85c..398fc5cee 100644 --- a/tests/lean/simp32.lean +++ b/tests/lean/simp32.lean @@ -20,7 +20,6 @@ variable f {A : Type} : A → A local m = simplifier_monitor(nil, nil, nil, function (s, e, i, k) print("App simplification failure, argument #" .. i) - print(e) print("Kind: " .. k) print("-----------") end, diff --git a/tests/lean/simp32.lean.expected.out b/tests/lean/simp32.lean.expected.out index 4e31cb177..3d469f871 100644 --- a/tests/lean/simp32.lean.expected.out +++ b/tests/lean/simp32.lean.expected.out @@ -10,7 +10,6 @@ λ val : ℕ, (λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val == (λ (n : ℕ) (v : vec (n + 0)), v) val =====> App simplification failure, argument #2 -(λ (n : ℕ) (v : vec (n + 0)), f v ; empty) 2::1 == (λ (n : ℕ) (v : vec (n + 0)), v) 2::1 Kind: 0 ----------- λ val : ℕ, (λ (n : ℕ) (v : vec (n + 0)), f v ; empty) val == (λ (n : ℕ) (v : vec (n + 0)), v) val