diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean index 551446308b46..49bb597934c3 100644 --- a/tests/lean/run/grind_pre.lean +++ b/tests/lean/run/grind_pre.lean @@ -21,24 +21,6 @@ theorem ex (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by open Lean.Grind.Eager in /-- error: `grind` failed -a b c : Bool -p q : Prop -left✝ : a = true -h✝ : b = true -left : p -right : q -h : b = false -⊢ False - -a b c : Bool -p q : Prop -left✝ : a = true -h✝ : b = true -left : p -right : q -h : a = false -⊢ False - a b c : Bool p q : Prop left✝ : a = true @@ -47,15 +29,6 @@ left : p right : q h : b = false ⊢ False - -a b c : Bool -p q : Prop -left✝ : a = true -h✝ : c = true -left : p -right : q -h : a = false -⊢ False -/ #guard_msgs (error) in theorem ex2 (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by