DefEqTransformations
📁 Source: Mathlib/Tactic/DefEqTransformations.lean
Statistics
| Metric | Count |
|---|---|
DefinitionschangeLocalDecl', betaReduceStx, convBeta_reduce, convEta_expand, convEta_reduce, convEta_struct, convRefold_let___, convUnfold_projs, etaExpandAll, etaExpandStx, etaReduceAll, etaReduceStx, etaStruct?, etaStructAll, etaStructStx, getProjectedExpr, refoldFVars, refoldLetStx, runDefEqConvTactic, runDefEqTactic, tacticReduce__, tacticWhnf__, unfoldFVars, unfoldProjs, unfoldProjsStx | 25 |
| Theorems | 0 |
| Total | 25 |
Lean.MVarId
Definitions
| Name | Category | Theorems |
|---|---|---|
changeLocalDecl' 📖 | CompOp | — |
Mathlib.Tactic
Definitions
| Name | Category | Theorems |
|---|---|---|
betaReduceStx 📖 | CompOp | — |
convBeta_reduce 📖 | CompOp | — |
convEta_expand 📖 | CompOp | — |
convEta_reduce 📖 | CompOp | — |
convEta_struct 📖 | CompOp | — |
convRefold_let___ 📖 | CompOp | — |
convUnfold_projs 📖 | CompOp | — |
etaExpandAll 📖 | CompOp | — |
etaExpandStx 📖 | CompOp | — |
etaReduceAll 📖 | CompOp | — |
etaReduceStx 📖 | CompOp | — |
etaStruct? 📖 | CompOp | — |
etaStructAll 📖 | CompOp | — |
etaStructStx 📖 | CompOp | — |
getProjectedExpr 📖 | CompOp | — |
refoldFVars 📖 | CompOp | — |
refoldLetStx 📖 | CompOp | — |
runDefEqConvTactic 📖 | CompOp | — |
runDefEqTactic 📖 | CompOp | — |
tacticReduce__ 📖 | CompOp | — |
tacticWhnf__ 📖 | CompOp | — |
unfoldFVars 📖 | CompOp | — |
unfoldProjs 📖 | CompOp | — |
unfoldProjsStx 📖 | CompOp | — |
---