Basic
📁 Source: Aesop/Builder/Basic.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsCoreRuleBuilderOutput, builderName, indexingMode, pattern?, ruleExprName, scopeName, tac, PhaseSpec, phase, toRule, RuleBuilder, RuleBuilderInput, options, phase, phaseName, term, RuleBuilderOptions, casesPatterns?, default, immediatePremises?, indexTransparency?, indexingMode?, instEmptyCollection, pattern?, transparency?, elabGlobalRuleIdent, elabInductiveRuleIdent, instInhabitedPhaseSpec, default, instInhabitedRuleBuilderInput, default, instInhabitedRuleBuilderOptions, default | 33 |
| Theorems | 0 |
| Total | 33 |
Aesop
Definitions
| Name | Category | Theorems |
|---|---|---|
CoreRuleBuilderOutput 📖 | CompData | — |
PhaseSpec 📖 | CompData | — |
RuleBuilder 📖 | CompOp | — |
RuleBuilderInput 📖 | CompData | — |
RuleBuilderOptions 📖 | CompData | — |
elabGlobalRuleIdent 📖 | CompOp | — |
elabInductiveRuleIdent 📖 | CompOp | — |
instInhabitedPhaseSpec 📖 | CompOp | — |
instInhabitedRuleBuilderInput 📖 | CompOp | — |
instInhabitedRuleBuilderOptions 📖 | CompOp | — |
Aesop.CoreRuleBuilderOutput
Definitions
| Name | Category | Theorems |
|---|---|---|
builderName 📖 | CompOp | — |
indexingMode 📖 | CompOp | — |
pattern? 📖 | CompOp | — |
ruleExprName 📖 | CompOp | — |
scopeName 📖 | CompOp | — |
tac 📖 | CompOp | — |
Aesop.PhaseSpec
Definitions
| Name | Category | Theorems |
|---|---|---|
phase 📖 | CompOp | — |
toRule 📖 | CompOp | — |
Aesop.RuleBuilderInput
Definitions
| Name | Category | Theorems |
|---|---|---|
options 📖 | CompOp | — |
phase 📖 | CompOp | — |
phaseName 📖 | CompOp | — |
term 📖 | CompOp | — |
Aesop.RuleBuilderOptions
Definitions
| Name | Category | Theorems |
|---|---|---|
casesPatterns? 📖 | CompOp | — |
default 📖 | CompOp | — |
immediatePremises? 📖 | CompOp | — |
indexTransparency? 📖 | CompOp | — |
indexingMode? 📖 | CompOp | — |
instEmptyCollection 📖 | CompOp | — |
pattern? 📖 | CompOp | — |
transparency? 📖 | CompOp | — |
Aesop.instInhabitedPhaseSpec
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Aesop.instInhabitedRuleBuilderInput
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Aesop.instInhabitedRuleBuilderOptions
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
---