Alias
📁 Source: Batteries/Tactic/Alias.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsAliasInfo, name, toString, aliasExt, aliasLR, getAliasInfo, instInhabitedAliasInfo, default, mkIffMpApp, setAliasInfo, setDeprecatedTarget | 11 |
| Theorems | 0 |
| Total | 11 |
Batteries.Tactic.Alias
Definitions
| Name | Category | Theorems |
|---|---|---|
AliasInfo 📖 | CompData | — |
aliasExt 📖 | CompOp | — |
aliasLR 📖 | CompOp | — |
getAliasInfo 📖 | CompOp | — |
instInhabitedAliasInfo 📖 | CompOp | — |
mkIffMpApp 📖 | CompOp | — |
setAliasInfo 📖 | CompOp | — |
setDeprecatedTarget 📖 | CompOp | — |
Batteries.Tactic.Alias.AliasInfo
Definitions
| Name | Category | Theorems |
|---|---|---|
name 📖 | CompOp | — |
toString 📖 | CompOp | — |
Batteries.Tactic.Alias.instInhabitedAliasInfo
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---