9e18eea271
This PR adds `mkBackwardRuleFromExpr` to create backward rules from expressions, complementing the existing `mkBackwardRuleFromDecl` which only works with declaration names. The new function enables creating backward rules from partially applied terms. For example, `mkBackwardRuleFromExpr (mkApp (mkConst ``Exists.intro [1]) Nat.mkType)` creates a rule for `Exists.intro` with the type parameter fixed to `Nat`, leaving only the witness and proof as subgoals. The `levelParams` parameter supports universe polymorphism: when creating a rule like `Prod.mk Nat` that should work at multiple universe levels, the caller specifies which level parameters remain polymorphic. The pattern's universe variables are then instantiated appropriately at each application site. Also refactors `Pattern.lean` to share code between declaration-based and expression-based pattern creation, extracting `mkPatternFromType` and `mkEqPatternFromType` as common helpers. |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||