d748b0c8c9
This PR implements parameter optimization for the generated `instantiate` tactics produced by `finish?`. We use a simple parameter optimizer that takes two sets as input: the lower and upper bounds. The lower bound consists of the theorems actually used in the proof term, while the upper bound includes all the theorems instantiated in a particular theorem instantiation step. The lower bound is often sufficient to replay the proof, but in some cases, additional theorems must be included because a theorem instantiation may contribute to the proof by providing terms and many not be present in the final proof term. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||