max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: missing withReducible

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-09 18:30:36 -07:00
parent f5a4b30d5f
commit 87f49be5dd
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Meta/Tactic/Split.lean
View file

@ -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