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

chore: improve condition

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-24 12:37:11 -07:00
parent 84926f62ea
commit e8c1647fa5
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Elab/PreDefinition/Structural.lean
View file

@ -245,7 +245,8 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
let matcherApp? ← matchMatcherApp? e
match matcherApp? with
| some matcherApp =>
if !containsRecFn recFnName e then
/- If none of the alternatives contain a recursive application, we process it as a regular one. -/
if matcherApp.alts.all fun alt => !containsRecFn recFnName alt then
processApp e
else
/- Here is an example we currently not handle