24f550fd6f
This is part of #3983. After #4154 introduced equational lemmas for non-recursive functions and #5055 unififed the lemmas for structural and wf recursive funcitons, this now disables the special handling of recursive functions in `findMatchToSplit?`, so that the equational lemmas should be the same no matter how the function was defined. The new option `eqns.deepRecursiveSplit` can be disabled to get the old behavior. ### Breaking change This can break existing code, as there now can be extra equational lemmas: * Explicit uses of `f.eq_2` might have to be adjusted if the numbering changed. * Uses of `rw [f]` or `simp [f]` may no longer apply if they previously matched (and introduced a `match` statement), when the equational lemmas got more fine-grained. In this case either case analysis on the parameters before rewriting helps, or setting the option `opt.deepRecursiveSplit false` while defining the function |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||