GeneralizeProofs
📁 Source: Batteries/Tactic/GeneralizeProofs.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsAContext, config, depth, fvars, initLCtx, propToFVar, AState, generalizations, propToProof, Config, abstract, debug, maxDepth, GState, propToFVar, MAbs, findProof?, insertProof, withLocal, withRecurse, MGen, insertFVar, runMAbs, abstractProofs, appArgExpectedTypes, elabConfig, generalizeProofsCore, initialPropToFVar, mkLambdaFVarsUsedOnly, withGeneralizedProofs, generalizeProofsElab, generalizeProofs | 32 |
| Theorems | 0 |
| Total | 32 |
Batteries.Tactic
Definitions
| Name | Category | Theorems |
|---|---|---|
generalizeProofsElab 📖 | CompOp | — |
Batteries.Tactic.GeneralizeProofs
Definitions
| Name | Category | Theorems |
|---|---|---|
AContext 📖 | CompData | — |
AState 📖 | CompData | — |
Config 📖 | CompData | — |
GState 📖 | CompData | — |
MAbs 📖 | CompOp | — |
MGen 📖 | CompOp | — |
abstractProofs 📖 | CompOp | — |
appArgExpectedTypes 📖 | CompOp | — |
elabConfig 📖 | CompOp | — |
generalizeProofsCore 📖 | CompOp | — |
initialPropToFVar 📖 | CompOp | — |
mkLambdaFVarsUsedOnly 📖 | CompOp | — |
withGeneralizedProofs 📖 | CompOp | — |
Batteries.Tactic.GeneralizeProofs.AContext
Definitions
| Name | Category | Theorems |
|---|---|---|
config 📖 | CompOp | — |
depth 📖 | CompOp | — |
fvars 📖 | CompOp | — |
initLCtx 📖 | CompOp | — |
propToFVar 📖 | CompOp | — |
Batteries.Tactic.GeneralizeProofs.AState
Definitions
| Name | Category | Theorems |
|---|---|---|
generalizations 📖 | CompOp | — |
propToProof 📖 | CompOp | — |
Batteries.Tactic.GeneralizeProofs.Config
Definitions
| Name | Category | Theorems |
|---|---|---|
abstract 📖 | CompOp | — |
debug 📖 | CompOp | — |
maxDepth 📖 | CompOp | — |
Batteries.Tactic.GeneralizeProofs.GState
Definitions
| Name | Category | Theorems |
|---|---|---|
propToFVar 📖 | CompOp | — |
Batteries.Tactic.GeneralizeProofs.MAbs
Definitions
| Name | Category | Theorems |
|---|---|---|
findProof? 📖 | CompOp | — |
insertProof 📖 | CompOp | — |
withLocal 📖 | CompOp | — |
withRecurse 📖 | CompOp | — |
Batteries.Tactic.GeneralizeProofs.MGen
Definitions
| Name | Category | Theorems |
|---|---|---|
insertFVar 📖 | CompOp | — |
runMAbs 📖 | CompOp | — |
Lean.MVarId
Definitions
| Name | Category | Theorems |
|---|---|---|
generalizeProofs 📖 | CompOp | — |
---