3569797377
This PR adds `foo.fun_cases`, an automatically generated theorem that splits the goal according to the branching structure of `foo`, much like the Functional Induction Principle, but for all functions (not just recursive ones), and without providing inductive hypotheses. The design isn't quite final yet as to which function parameters should become targets of the motive, and which parameters of the theorem, but the current version is already proven to be useful, so start with this and iterate later. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||