409c6cac4c
Recursive predefinitions contains “rec app” markers as mdata in the predefinitions, but sometimes these get in the way of termination checking, when you have ``` [mdata (fun x => f)] arg ``` Therefore, the `preprocess` pass floats them out of applications (originally only for structural recursion, since #2818 also for well-founded recursion). But the code was incomplete: Because `Meta.transform` calls `post` on `f x y` only once (and not also on `f x`) one has to float out of nested applications as well. A consequence of this can be that in a recursive proof, `rw [foo]` does not work although `rw [foo _ _]` does. Also adding the testcase where @david-christiansen and I stumbled over this (Maybe the two preprocess modules can be combined, now that #2973 is landed, will try that in a follow-up). |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||