From 87f49be5ddca9a526fc8e9f7ab7e6720ad66c267 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 Sep 2021 18:30:36 -0700 Subject: [PATCH] fix: missing `withReducible` --- src/Lean/Meta/Tactic/Split.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index 7e4b2efa67..034fb7eee6 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -32,7 +32,7 @@ where | none => for matchEq in (← Match.getEquationsFor app.matcherName).eqnNames do -- Try lemma - match (← Simp.tryLemma? e { proof := mkConst matchEq, name? := some matchEq } SplitIf.discharge?) with + match (← withReducible <| Simp.tryLemma? e { proof := mkConst matchEq, name? := some matchEq } SplitIf.discharge?) with | none => pure () | some r => return Simp.Step.done r return Simp.Step.visit { expr := e } @@ -47,7 +47,7 @@ where | some e' => return Simp.Step.done { expr := e' } | none => -- Try lemma - match (← Simp.tryLemma? e { proof := mkConst matchEqDeclName, name? := matchEqDeclName } SplitIf.discharge?) with + match (← withReducible <| Simp.tryLemma? e { proof := mkConst matchEqDeclName, name? := matchEqDeclName } SplitIf.discharge?) with | none => return Simp.Step.visit { expr := e } | some r => return Simp.Step.done r else