FunctionData
📁 Source: Mathlib/Tactic/FunProp/FunctionData.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsFunctionData, args, decompositionOverArgs, domainType, fn, getFnConstName?, insts, isConstantFun, isIdentityFun, isMorApplication, lctx, mainArgs, mainVar, nontrivialDecomposition, peeloffArgDecomposition, toExpr, unfoldHeadFVar?, MaybeFunctionData, get, MorApplication, getFunctionData, getFunctionData?, instBEqMorApplication, beq, instInhabitedMorApplication, default | 26 |
| Theorems | 0 |
| Total | 26 |
Mathlib.Meta.FunProp
Definitions
| Name | Category | Theorems |
|---|---|---|
FunctionData 📖 | CompData | — |
MaybeFunctionData 📖 | CompData | — |
MorApplication 📖 | CompData | — |
getFunctionData 📖 | CompOp | — |
getFunctionData? 📖 | CompOp | — |
instBEqMorApplication 📖 | CompOp | — |
instInhabitedMorApplication 📖 | CompOp | — |
Mathlib.Meta.FunProp.FunctionData
Definitions
| Name | Category | Theorems |
|---|---|---|
args 📖 | CompOp | — |
decompositionOverArgs 📖 | CompOp | — |
domainType 📖 | CompOp | — |
fn 📖 | CompOp | — |
getFnConstName? 📖 | CompOp | — |
insts 📖 | CompOp | — |
isConstantFun 📖 | CompOp | — |
isIdentityFun 📖 | CompOp | — |
isMorApplication 📖 | CompOp | — |
lctx 📖 | CompOp | — |
mainArgs 📖 | CompOp | — |
mainVar 📖 | CompOp | — |
nontrivialDecomposition 📖 | CompOp | — |
peeloffArgDecomposition 📖 | CompOp | — |
toExpr 📖 | CompOp | — |
unfoldHeadFVar? 📖 | CompOp | — |
Mathlib.Meta.FunProp.MaybeFunctionData
Definitions
| Name | Category | Theorems |
|---|---|---|
get 📖 | CompOp | — |
Mathlib.Meta.FunProp.instBEqMorApplication
Definitions
| Name | Category | Theorems |
|---|---|---|
beq 📖 | CompOp | — |
Mathlib.Meta.FunProp.instInhabitedMorApplication
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---