RuleExpr

📁 Source: Aesop/Frontend/RuleExpr.lean

Statistics

Metric	Count
Definitions BuilderOption, elab, elab, DBuilderName, elab, instToString, toBuilderName?, toRuleBuilder, Feature, elab, elab, quot, quot, quot, quot, quot, quot, quot, builder_nameApply, builder_nameCases, builder_nameConstructors, builder_nameDefault, builder_nameDestruct, builder_nameForward, builder_nameSimp, builder_nameTactic, builder_nameUnfold, featIdent, feature_, feature__1, feature__2, feature__3, feature__4, indexing_modeHyp_, indexing_modeTarget_, indexing_modeUnindexed, phaseNorm, phaseSafe, phaseUnsafe, ruleSetsFeature, rule_expr_, rule_expr___, transparency, «builder_option(Cases_patterns:=[_])»»), «builder_option(Immediate:=[_])»»), «builder_option(Index:=[_])»»), «builder_option(Pattern:=_)»»), «builder_option(Transparency!:=_)»»), «builder_option(Transparency:=_)»»), «feature(_)»»), «priority-_», «priority_%», «rule_expr_[_]», elab, Priority, elab, instToString, toInt?, toPercent?, RuleConfig, addFeature, buildGlobalRule, buildLocalRule, buildRule, builder?, builderOptions, getBuilder, getPenalty, getPhase, getPhaseSpec, getRuleBuilderInput, getSimpPriority, getSuccessProbability, getTerm, phase?, priority?, ruleSets, term?, toRuleFilter, validateForAdditionalRules, RuleExpr, buildAdditionalGlobalRules, buildAdditionalLocalRules, elab, foldBranchesM, toAdditionalGlobalRules, toAdditionalLocalRules, toAdditionalRules, toGlobalRuleFilters, toLocalRuleFilters, toRuleConfigs, toRuleFilters, elab, RuleSets, elab, ruleSets, addBuilderOption, elabSingleIndexingMode, elabTransparency, instInhabitedDBuilderName, default, instInhabitedFeature, default, instInhabitedPriority, default, instInhabitedRuleExpr, default, instInhabitedRuleSets, default, builder_name, builder_option, feature, indexing_mode, phase, priority, rule_expr	116
Theorems	0
Total	116

Aesop.Frontend

Definitions

Name	Category	Theorems
BuilderOption 📖	CompData	—
DBuilderName 📖	CompData	—
Feature 📖	CompData	—
Priority 📖	CompData	—
RuleConfig 📖	CompData	—
RuleExpr 📖	CompData	—
RuleSets 📖	CompData	—
addBuilderOption 📖	CompOp	—
elabSingleIndexingMode 📖	CompOp	—
elabTransparency 📖	CompOp	—
instInhabitedDBuilderName 📖	CompOp	—
instInhabitedFeature 📖	CompOp	—
instInhabitedPriority 📖	CompOp	—
instInhabitedRuleExpr 📖	CompOp	—
instInhabitedRuleSets 📖	CompOp	—

Aesop.Frontend.BuilderOption

Definitions

Name	Category	Theorems
elab 📖	CompOp	—

Aesop.Frontend.CasesPattern

Definitions

Name	Category	Theorems
elab 📖	CompOp	—

Aesop.Frontend.DBuilderName

Definitions

Name	Category	Theorems
elab 📖	CompOp	—
instToString 📖	CompOp	—
toBuilderName? 📖	CompOp	—
toRuleBuilder 📖	CompOp	—

Aesop.Frontend.Feature

Definitions

Name	Category	Theorems
elab 📖	CompOp	—

Aesop.Frontend.IndexingMode

Definitions

Name	Category	Theorems
elab 📖	CompOp	—

Aesop.Frontend.Parser

Definitions

Name	Category	Theorems
builder_nameApply 📖	CompOp	—
builder_nameCases 📖	CompOp	—
builder_nameConstructors 📖	CompOp	—
builder_nameDefault 📖	CompOp	—
builder_nameDestruct 📖	CompOp	—
builder_nameForward 📖	CompOp	—
builder_nameSimp 📖	CompOp	—
builder_nameTactic 📖	CompOp	—
builder_nameUnfold 📖	CompOp	—
featIdent 📖	CompOp	—
feature_ 📖	CompOp	—
feature__1 📖	CompOp	—
feature__2 📖	CompOp	—
feature__3 📖	CompOp	—
feature__4 📖	CompOp	—
indexing_modeHyp_ 📖	CompOp	—
indexing_modeTarget_ 📖	CompOp	—
indexing_modeUnindexed 📖	CompOp	—
phaseNorm 📖	CompOp	—
phaseSafe 📖	CompOp	—
phaseUnsafe 📖	CompOp	—
ruleSetsFeature 📖	CompOp	—
rule_expr_ 📖	CompOp	—
rule_expr___ 📖	CompOp	—
transparency 📖	CompOp	—
«builder_option(Cases_patterns:=[_])» 📖» "API Documentation")	CompOp	—
«builder_option(Immediate:=[_])» 📖» "API Documentation")	CompOp	—
«builder_option(Index:=[_])» 📖» "API Documentation")	CompOp	—
«builder_option(Pattern:=_)» 📖» "API Documentation")	CompOp	—
«builder_option(Transparency!:=_)» 📖» "API Documentation")	CompOp	—
«builder_option(Transparency:=_)» 📖» "API Documentation")	CompOp	—
«feature(_)» 📖» "API Documentation")	CompOp	—
«priority-_» 📖	CompOp	—
«priority_%» 📖	CompOp	—
«rule_expr_[_]» 📖	CompOp	—

Aesop.Frontend.Parser.Aesop.builder_name

Definitions

Name	Category	Theorems
quot 📖	CompOp	—

Aesop.Frontend.Parser.Aesop.builder_option

Definitions

Name	Category	Theorems
quot 📖	CompOp	—

Aesop.Frontend.Parser.Aesop.feature

Definitions

Name	Category	Theorems
quot 📖	CompOp	—

Aesop.Frontend.Parser.Aesop.indexing_mode

Definitions

Name	Category	Theorems
quot 📖	CompOp	—

Aesop.Frontend.Parser.Aesop.phase

Definitions

Name	Category	Theorems
quot 📖	CompOp	—

Aesop.Frontend.Parser.Aesop.priority

Definitions

Name	Category	Theorems
quot 📖	CompOp	—

Aesop.Frontend.Parser.Aesop.rule_expr

Definitions

Name	Category	Theorems
quot 📖	CompOp	—

Aesop.Frontend.PhaseName

Definitions

Name	Category	Theorems
elab 📖	CompOp	—

Aesop.Frontend.Priority

Definitions

Name	Category	Theorems
elab 📖	CompOp	—
instToString 📖	CompOp	—
toInt? 📖	CompOp	—
toPercent? 📖	CompOp	—

Aesop.Frontend.RuleConfig

Definitions

Name	Category	Theorems
addFeature 📖	CompOp	—
buildGlobalRule 📖	CompOp	—
buildLocalRule 📖	CompOp	—
buildRule 📖	CompOp	—
builder? 📖	CompOp	—
builderOptions 📖	CompOp	—
getBuilder 📖	CompOp	—
getPenalty 📖	CompOp	—
getPhase 📖	CompOp	—
getPhaseSpec 📖	CompOp	—
getRuleBuilderInput 📖	CompOp	—
getSimpPriority 📖	CompOp	—
getSuccessProbability 📖	CompOp	—
getTerm 📖	CompOp	—
phase? 📖	CompOp	—
priority? 📖	CompOp	—
ruleSets 📖	CompOp	—
term? 📖	CompOp	—
toRuleFilter 📖	CompOp	—
validateForAdditionalRules 📖	CompOp	—

Aesop.Frontend.RuleExpr

Definitions

Name	Category	Theorems
buildAdditionalGlobalRules 📖	CompOp	—
buildAdditionalLocalRules 📖	CompOp	—
elab 📖	CompOp	—
foldBranchesM 📖	CompOp	—
toAdditionalGlobalRules 📖	CompOp	—
toAdditionalLocalRules 📖	CompOp	—
toAdditionalRules 📖	CompOp	—
toGlobalRuleFilters 📖	CompOp	—
toLocalRuleFilters 📖	CompOp	—
toRuleConfigs 📖	CompOp	—
toRuleFilters 📖	CompOp	—

Aesop.Frontend.RuleSetName

Definitions

Name	Category	Theorems
elab 📖	CompOp	—

Aesop.Frontend.RuleSets

Definitions

Name	Category	Theorems
elab 📖	CompOp	—
ruleSets 📖	CompOp	—

Aesop.Frontend.instInhabitedDBuilderName

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.Frontend.instInhabitedFeature

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.Frontend.instInhabitedPriority

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.Frontend.instInhabitedRuleExpr

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Aesop.Frontend.instInhabitedRuleSets

Definitions

Name	Category	Theorems
default 📖	CompOp	—

Lean.Parser.Category.Aesop

Definitions

Name	Category	Theorems
builder_name 📖	CompOp	—
builder_option 📖	CompOp	—
feature 📖	CompOp	—
indexing_mode 📖	CompOp	—
phase 📖	CompOp	—
priority 📖	CompOp	—
rule_expr 📖	CompOp	—

---

← Back to Index