FVarIdSubst
📁 Source: Aesop/RuleTac/FVarIdSubst.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsFVarIdSubst, append, apply, applyToLocalDecl, codomain, contains, domain, empty, erase, find?, get, insert, instEmptyCollection, isEmpty, map, ofFVarSubst?, ofFVarSubstIgnoringNonFVarIds, instInhabitedFVarIdSubst, default | 19 |
| Theorems | 0 |
| Total | 19 |
Aesop
Definitions
| Name | Category | Theorems |
|---|---|---|
FVarIdSubst 📖 | CompData | — |
instInhabitedFVarIdSubst 📖 | CompOp | — |
Aesop.FVarIdSubst
Definitions
| Name | Category | Theorems |
|---|---|---|
append 📖 | CompOp | — |
apply 📖 | CompOp | — |
applyToLocalDecl 📖 | CompOp | — |
codomain 📖 | CompOp | — |
contains 📖 | CompOp | — |
domain 📖 | CompOp | — |
empty 📖 | CompOp | — |
erase 📖 | CompOp | — |
find? 📖 | CompOp | — |
get 📖 | CompOp | — |
insert 📖 | CompOp | — |
instEmptyCollection 📖 | CompOp | — |
isEmpty 📖 | CompOp | — |
map 📖 | CompOp | — |
ofFVarSubst? 📖 | CompOp | — |
ofFVarSubstIgnoringNonFVarIds 📖 | CompOp | — |
Aesop.instInhabitedFVarIdSubst
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---