Mor
📁 Source: Mathlib/Tactic/FunProp/Mor.lean
Statistics
| Metric | Count |
|---|---|
| 17 | |
| Theorems | 0 |
| Total | 17 |
Mathlib.Meta.FunProp
Definitions
| Name | Category | Theorems |
|---|---|---|
Forall 📖 | CompOp | — |
Mathlib.Meta.FunProp.Mor
Definitions
| Name | Category | Theorems |
|---|---|---|
App 📖 | CompData | — |
app 📖 | CompOp | — |
getAppArgs 📖 | CompOp | — |
getAppFn 📖 | CompOp | — |
instInhabitedArg 📖 | CompOp | — |
isCoeFun 📖 | CompOp | — |
isCoeFunName 📖 | CompOp | — |
isMorApp? 📖 | CompOp | — |
mkAppN 📖 | CompOp | — |
whnf 📖 | CompOp | — |
whnfPred 📖 | CompOp | — |
withApp 📖 | CompOp | — |
Mathlib.Meta.FunProp.Mor.App
Definitions
| Name | Category | Theorems |
|---|---|---|
arg 📖 | CompOp | — |
fn 📖 | CompOp | — |
Mathlib.Meta.FunProp.Mor.Arg
Definitions
| Name | Category | Theorems |
|---|---|---|
expr 📖 | CompOp | — |
Mathlib.Meta.FunProp.Mor.instInhabitedArg
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---