ProdAssoc
📁 Source: Mathlib/Tactic/ProdAssoc.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsProdTree, components, convertTo, getType, pack, size, unpack, elabProdAssoc, instReprProdTree, repr, mkProdEquiv, mkProdFun, mkProdTree, prodAssocStx, «termProd_assoc%» | 15 |
| Theorems | 0 |
| Total | 15 |
Lean.Expr
Definitions
| Name | Category | Theorems |
|---|---|---|
ProdTree 📖 | CompData | — |
elabProdAssoc 📖 | CompOp | — |
instReprProdTree 📖 | CompOp | — |
mkProdEquiv 📖 | CompOp | — |
mkProdFun 📖 | CompOp | — |
mkProdTree 📖 | CompOp | — |
prodAssocStx 📖 | CompOp | — |
«termProd_assoc%» 📖 | CompOp | — |
Lean.Expr.ProdTree
Definitions
| Name | Category | Theorems |
|---|---|---|
components 📖 | CompOp | — |
convertTo 📖 | CompOp | — |
getType 📖 | CompOp | — |
pack 📖 | CompOp | — |
size 📖 | CompOp | — |
unpack 📖 | CompOp | — |
Lean.Expr.instReprProdTree
Definitions
| Name | Category | Theorems |
|---|---|---|
repr 📖 | CompOp | — |
---