FBinop
📁 Source: Mathlib/Tactic/FBinop.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsSRec, args, name, elabBinOp, instInhabitedSRec, default, instToExprSRec, toExpr, prodSyntax | 9 |
| Theorems | 0 |
| Total | 9 |
FBinopElab
Definitions
| Name | Category | Theorems |
|---|---|---|
SRec 📖 | CompData | — |
elabBinOp 📖 | CompOp | — |
instInhabitedSRec 📖 | CompOp | — |
instToExprSRec 📖 | CompOp | — |
prodSyntax 📖 | CompOp | — |
FBinopElab.SRec
Definitions
| Name | Category | Theorems |
|---|---|---|
args 📖 | CompOp | — |
name 📖 | CompOp | — |
FBinopElab.instInhabitedSRec
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
FBinopElab.instToExprSRec
Definitions
| Name | Category | Theorems |
|---|---|---|
toExpr 📖 | CompOp | — |
---