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

feat: use splitTarget? when proving equation theorems for recursive definitions

Browse source
This commit is contained in:
Leonardo de Moura 2022-02-08 12:53:09 -08:00
parent afb5cb16ee
commit 3367f0b06a
2 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/PreDefinition/Structural/Eqns.lean
View file

@ -50,6 +50,8 @@ where
go mvarId
else if let some mvarIds ← casesOnStuckLHS? mvarId then
mvarIds.forM go
else if let some mvarIds ← splitTarget? mvarId then
mvarIds.forM go
else
throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"

2
src/Lean/Elab/PreDefinition/WF/Eqns.lean
View file

@ -57,6 +57,8 @@ where
| TacticResultCNM.noChange =>
if let some mvarIds ← casesOnStuckLHS? mvarId then
mvarIds.forM go
else if let some mvarIds ← splitTarget? mvarId then
mvarIds.forM go
else
throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"