Decl
📁 Source: Mathlib/Tactic/FunProp/Decl.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsFunPropDecl, funArgId, funPropName, path, FunPropDecls, decls, FunPropDeclsExt, addFunPropDecl, funPropDeclsExt, getFunProp?, getFunPropDecl?, getFunPropFun?, instBEqFunPropDecl, beq, instInhabitedFunPropDecl, default, instInhabitedFunPropDecls, default, isFunProp, isFunPropGoal, tacticToDischarge | 21 |
| Theorems | 0 |
| Total | 21 |
Mathlib.Meta.FunProp
Definitions
| Name | Category | Theorems |
|---|---|---|
FunPropDecl 📖 | CompData | — |
FunPropDecls 📖 | CompData | — |
FunPropDeclsExt 📖 | CompOp | — |
addFunPropDecl 📖 | CompOp | — |
funPropDeclsExt 📖 | CompOp | — |
getFunProp? 📖 | CompOp | — |
getFunPropDecl? 📖 | CompOp | — |
getFunPropFun? 📖 | CompOp | — |
instBEqFunPropDecl 📖 | CompOp | — |
instInhabitedFunPropDecl 📖 | CompOp | — |
instInhabitedFunPropDecls 📖 | CompOp | — |
isFunProp 📖 | CompOp | — |
isFunPropGoal 📖 | CompOp | — |
tacticToDischarge 📖 | CompOp | — |
Mathlib.Meta.FunProp.FunPropDecl
Definitions
| Name | Category | Theorems |
|---|---|---|
funArgId 📖 | CompOp | — |
funPropName 📖 | CompOp | — |
path 📖 | CompOp | — |
Mathlib.Meta.FunProp.FunPropDecls
Definitions
| Name | Category | Theorems |
|---|---|---|
decls 📖 | CompOp | — |
Mathlib.Meta.FunProp.instBEqFunPropDecl
Definitions
| Name | Category | Theorems |
|---|---|---|
beq 📖 | CompOp | — |
Mathlib.Meta.FunProp.instInhabitedFunPropDecl
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Mathlib.Meta.FunProp.instInhabitedFunPropDecls
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---