TermCongr
📁 Source: Mathlib/Tactic/TermCongr.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsCongrResult, defeq, eq, heq, iff, isRfl, lhs, mk', mkDefault, mkDefault', pf?, rhs, trans, CongrType, cHole, cHole?, cHoleExpand, elabCHole, elabCHoleExpand, elabTermCongr, elaboratePattern, ensureIff, hasCHole, mkCHole, mkCongrOf, mkCongrOfApp, mkCongrOfAux, mkCongrOfCHole?, mkEqForExpectedType, mkHEqForExpectedType, mkIffForExpectedType, processAntiquot, removeCHoles, termCongr, throwCongrEx, unexpandCHole | 36 |
| Theorems | 0 |
| Total | 36 |
Mathlib.Tactic.TermCongr
Definitions
| Name | Category | Theorems |
|---|---|---|
CongrResult 📖 | CompData | — |
CongrType 📖 | CompData | — |
cHole 📖 | CompOp | — |
cHole? 📖 | CompOp | — |
cHoleExpand 📖 | CompOp | — |
elabCHole 📖 | CompOp | — |
elabCHoleExpand 📖 | CompOp | — |
elabTermCongr 📖 | CompOp | — |
elaboratePattern 📖 | CompOp | — |
ensureIff 📖 | CompOp | — |
hasCHole 📖 | CompOp | — |
mkCHole 📖 | CompOp | — |
mkCongrOf 📖 | CompOp | — |
mkCongrOfApp 📖 | CompOp | — |
mkCongrOfAux 📖 | CompOp | — |
mkCongrOfCHole? 📖 | CompOp | — |
mkEqForExpectedType 📖 | CompOp | — |
mkHEqForExpectedType 📖 | CompOp | — |
mkIffForExpectedType 📖 | CompOp | — |
processAntiquot 📖 | CompOp | — |
removeCHoles 📖 | CompOp | — |
termCongr 📖 | CompOp | — |
throwCongrEx 📖 | CompOp | — |
unexpandCHole 📖 | CompOp | — |
Mathlib.Tactic.TermCongr.CongrResult
Definitions
| Name | Category | Theorems |
|---|---|---|
defeq 📖 | CompOp | — |
eq 📖 | CompOp | — |
heq 📖 | CompOp | — |
iff 📖 | CompOp | — |
isRfl 📖 | CompOp | — |
lhs 📖 | CompOp | — |
mk' 📖 | CompOp | — |
mkDefault 📖 | CompOp | — |
mkDefault' 📖 | CompOp | — |
pf? 📖 | CompOp | — |
rhs 📖 | CompOp | — |
trans 📖 | CompOp | — |
---