RulePattern
📁 Source: Aesop/Index/RulePattern.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsRulePatternIndex, Entry, name, pattern, add, get, getCore, getInGoal, getInLocalDecl, getInLocalDeclCore, getSingle, instEmptyCollection, instInhabitedEntry, default, isEmpty, merge, tree, RulePatternSubstMap, insertArray, ofArray, toFlatArray, instBEqEntry, instInhabitedRulePatternIndex, default | 24 |
| Theorems | 0 |
| Total | 24 |
Aesop
Definitions
| Name | Category | Theorems |
|---|---|---|
RulePatternIndex 📖 | CompData | — |
RulePatternSubstMap 📖 | CompOp | — |
instBEqEntry 📖 | CompOp | — |
instInhabitedRulePatternIndex 📖 | CompOp | — |
Aesop.RulePatternIndex
Definitions
| Name | Category | Theorems |
|---|---|---|
Entry 📖 | CompData | — |
add 📖 | CompOp | — |
get 📖 | CompOp | — |
getCore 📖 | CompOp | — |
getInGoal 📖 | CompOp | — |
getInLocalDecl 📖 | CompOp | — |
getInLocalDeclCore 📖 | CompOp | — |
getSingle 📖 | CompOp | — |
instEmptyCollection 📖 | CompOp | — |
instInhabitedEntry 📖 | CompOp | — |
isEmpty 📖 | CompOp | — |
merge 📖 | CompOp | — |
tree 📖 | CompOp | — |
Aesop.RulePatternIndex.Entry
Definitions
| Name | Category | Theorems |
|---|---|---|
name 📖 | CompOp | — |
pattern 📖 | CompOp | — |
Aesop.RulePatternIndex.instInhabitedEntry
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Aesop.RulePatternSubstMap
Definitions
| Name | Category | Theorems |
|---|---|---|
insertArray 📖 | CompOp | — |
ofArray 📖 | CompOp | — |
toFlatArray 📖 | CompOp | — |
Aesop.instInhabitedRulePatternIndex
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---