def Lean.Parser.Category.Aesop.priority : Category

def Aesop.Frontend.Parser.Aesop.priority.quot : Lean.ParserDescr

def Aesop.Frontend.Parser.«priority_%» : Lean.ParserDescr

def Aesop.Frontend.Parser.«priority-_» : Lean.ParserDescr

inductive Aesop.Frontend.Priority : Type

• int (i : Int) : Priority
• percent (p : Percent) : Priority

def Aesop.Frontend.instInhabitedPriority.default : Priority

@[implicit_reducible]

instance Aesop.Frontend.instInhabitedPriority : Inhabited Priority

def Aesop.Frontend.Priority.elab (stx : Lean.Syntax) : ElabM Priority

@[implicit_reducible]

instance Aesop.Frontend.Priority.instToString : ToString Priority

def Aesop.Frontend.Priority.toInt? : Priority → Option Int

def Aesop.Frontend.Priority.toPercent? : Priority → Option Percent

def Aesop.Frontend.Parser.Aesop.phase.quot : Lean.ParserDescr

def Lean.Parser.Category.Aesop.phase : Category

def Aesop.Frontend.Parser.phaseSafe : Lean.ParserDescr

def Aesop.Frontend.Parser.phaseNorm : Lean.ParserDescr

def Aesop.Frontend.Parser.phaseUnsafe : Lean.ParserDescr

def Aesop.Frontend.PhaseName.elab (stx : Lean.Syntax) : ElabM PhaseName

def Aesop.Frontend.Parser.Aesop.builder_name.quot : Lean.ParserDescr

def Lean.Parser.Category.Aesop.builder_name : Category

def Aesop.Frontend.Parser.builder_nameApply : Lean.ParserDescr

def Aesop.Frontend.Parser.builder_nameSimp : Lean.ParserDescr

def Aesop.Frontend.Parser.builder_nameUnfold : Lean.ParserDescr

def Aesop.Frontend.Parser.builder_nameTactic : Lean.ParserDescr

def Aesop.Frontend.Parser.builder_nameConstructors : Lean.ParserDescr

def Aesop.Frontend.Parser.builder_nameForward : Lean.ParserDescr

def Aesop.Frontend.Parser.builder_nameDestruct : Lean.ParserDescr

def Aesop.Frontend.Parser.builder_nameCases : Lean.ParserDescr

def Aesop.Frontend.Parser.builder_nameDefault : Lean.ParserDescr

inductive Aesop.Frontend.DBuilderName : Type

• regular (b : BuilderName) : DBuilderName
• default : DBuilderName

@[implicit_reducible]

instance Aesop.Frontend.instInhabitedDBuilderName : Inhabited DBuilderName

def Aesop.Frontend.instInhabitedDBuilderName.default : DBuilderName

def Aesop.Frontend.DBuilderName.elab (stx : Lean.Syntax) : ElabM DBuilderName

@[implicit_reducible]

instance Aesop.Frontend.DBuilderName.instToString : ToString DBuilderName

def Aesop.Frontend.DBuilderName.toBuilderName? : DBuilderName → Option BuilderName

def Aesop.Frontend.DBuilderName.toRuleBuilder : DBuilderName → RuleBuilder

def Lean.Parser.Category.Aesop.indexing_mode : Category

def Aesop.Frontend.Parser.Aesop.indexing_mode.quot : Lean.ParserDescr

def Aesop.Frontend.Parser.indexing_modeTarget_ : Lean.ParserDescr

def Aesop.Frontend.Parser.indexing_modeHyp_ : Lean.ParserDescr

def Aesop.Frontend.Parser.indexing_modeUnindexed : Lean.ParserDescr

def Aesop.Frontend.elabSingleIndexingMode (stx : Lean.Syntax) : ElabM IndexingMode

def Aesop.Frontend.IndexingMode.elab (stxs : Array Lean.Syntax) : ElabM IndexingMode

def Aesop.Frontend.CasesPattern.elab (stx : Lean.Syntax) : Lean.Elab.TermElabM CasesPattern

def Aesop.Frontend.Parser.transparency : Lean.ParserDescr

def Aesop.Frontend.elabTransparency : Lean.TSyntax `Aesop.Frontend.Parser.transparency → Lean.Elab.TermElabM Lean.Meta.TransparencyMode

def Lean.Parser.Category.Aesop.builder_option : Category

def Aesop.Frontend.Parser.Aesop.builder_option.quot : Lean.ParserDescr

def Aesop.Frontend.Parser.«builder_option(Immediate:=[_])» : Lean.ParserDescr

def Aesop.Frontend.Parser.«builder_option(Index:=[_])» : Lean.ParserDescr

def Aesop.Frontend.Parser.«builder_option(Pattern:=_)» : Lean.ParserDescr

def Aesop.Frontend.Parser.«builder_option(Cases_patterns:=[_])» : Lean.ParserDescr

def Aesop.Frontend.Parser.«builder_option(Transparency:=_)» : Lean.ParserDescr

def Aesop.Frontend.Parser.«builder_option(Transparency!:=_)» : Lean.ParserDescr

inductive Aesop.Frontend.BuilderOption : Type

• immediate (names : Array Lean.Name) : BuilderOption
• index (imode : IndexingMode) : BuilderOption
• pattern (stx : Lean.Term) : BuilderOption
• casesPatterns (pats : Array CasesPattern) : BuilderOption
• transparency (md : Lean.Meta.TransparencyMode) (alsoForIndex : Bool) : BuilderOption

def Aesop.Frontend.BuilderOption.elab (stx : Lean.TSyntax `Aesop.builder_option) : ElabM BuilderOption

def Aesop.Frontend.addBuilderOption (bos : RuleBuilderOptions) : BuilderOption → RuleBuilderOptions

def Aesop.Frontend.Parser.ruleSetsFeature : Lean.ParserDescr

def Aesop.Frontend.RuleSetName.elab (stx : Lean.Syntax) : RuleSetName

structure Aesop.Frontend.RuleSets : Type

• ruleSets : Array RuleSetName

@[implicit_reducible]

instance Aesop.Frontend.instInhabitedRuleSets : Inhabited RuleSets

def Aesop.Frontend.instInhabitedRuleSets.default : RuleSets

def Aesop.Frontend.RuleSets.elab (stx : Lean.Syntax) : ElabM RuleSets

def Aesop.Frontend.Parser.Aesop.feature.quot : Lean.ParserDescr

def Lean.Parser.Category.Aesop.feature : Category

def Aesop.Frontend.Parser.feature_ : Lean.ParserDescr

def Aesop.Frontend.Parser.feature__1 : Lean.ParserDescr

def Aesop.Frontend.Parser.feature__2 : Lean.ParserDescr

def Aesop.Frontend.Parser.feature__3 : Lean.ParserDescr

def Aesop.Frontend.Parser.feature__4 : Lean.ParserDescr

def Aesop.Frontend.Parser.featIdent : Lean.ParserDescr

def Aesop.Frontend.Parser.«feature(_)» : Lean.ParserDescr

inductive Aesop.Frontend.Feature : Type

• phase (p : PhaseName) : Feature
• priority (p : Priority) : Feature
• builder (b : DBuilderName) : Feature
• builderOption (o : BuilderOption) : Feature
• term (i : Lean.Term) : Feature
• ruleSets (rs : RuleSets) : Feature

def Aesop.Frontend.instInhabitedFeature.default : Feature

@[implicit_reducible]

instance Aesop.Frontend.instInhabitedFeature : Inhabited Feature

partial def Aesop.Frontend.Feature.elab (stx : Lean.Syntax) : ElabM Feature

def Aesop.Frontend.Parser.Aesop.rule_expr.quot : Lean.ParserDescr

def Lean.Parser.Category.Aesop.rule_expr : Category

def Aesop.Frontend.Parser.rule_expr_ : Lean.ParserDescr

def Aesop.Frontend.Parser.rule_expr___ : Lean.ParserDescr

def Aesop.Frontend.Parser.«rule_expr_[_]» : Lean.ParserDescr

inductive Aesop.Frontend.RuleExpr : Type

• node (f : Feature) (children : Array RuleExpr) : RuleExpr

@[implicit_reducible]

instance Aesop.Frontend.instInhabitedRuleExpr : Inhabited RuleExpr

def Aesop.Frontend.instInhabitedRuleExpr.default : RuleExpr

partial def Aesop.Frontend.RuleExpr.elab (stx : Lean.Syntax) : ElabM RuleExpr

def Aesop.Frontend.RuleExpr.foldBranchesM {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] (f : σ → Feature → m σ) (init : σ) (e : RuleExpr) : m (Array σ)

structure Aesop.Frontend.RuleConfig : Type

• term? : Option Lean.Term
• phase? : Option PhaseName
• priority? : Option Priority
• builder? : Option DBuilderName
• builderOptions : RuleBuilderOptions
• ruleSets : RuleSets

def Aesop.Frontend.RuleConfig.addFeature {m : Type → Type} [Monad m] [Lean.MonadError m] (c : RuleConfig) : Feature → m RuleConfig

def Aesop.Frontend.RuleConfig.getPenalty {m : Type → Type} [Monad m] [Lean.MonadError m] (phase : PhaseName) (c : RuleConfig) : m Int

def Aesop.Frontend.RuleConfig.getSuccessProbability {m : Type → Type} [Monad m] [Lean.MonadError m] (c : RuleConfig) : m Percent

def Aesop.Frontend.RuleConfig.getSimpPriority {m : Type → Type} [Monad m] [Lean.MonadError m] (c : RuleConfig) : m Nat

def Aesop.Frontend.RuleConfig.getTerm {m : Type → Type} [Monad m] [Lean.MonadError m] (c : RuleConfig) : m Lean.Term

def Aesop.Frontend.RuleConfig.getPhase {m : Type → Type} [Monad m] [Lean.MonadError m] (c : RuleConfig) : m PhaseName

def Aesop.Frontend.RuleConfig.getBuilder {m : Type → Type} [Monad m] [Lean.MonadError m] (c : RuleConfig) : m DBuilderName

def Aesop.Frontend.RuleConfig.getPhaseSpec {m : Type → Type} [Monad m] [Lean.MonadError m] (c : RuleConfig) : m PhaseSpec

def Aesop.Frontend.RuleConfig.getRuleBuilderInput (c : RuleConfig) : Lean.Elab.TermElabM RuleBuilderInput

def Aesop.Frontend.RuleConfig.buildRule (c : RuleConfig) : ElabM (LocalRuleSetMember × Array RuleSetName)

def Aesop.Frontend.RuleConfig.buildGlobalRule (c : RuleConfig) : ElabM (GlobalRuleSetMember × Array RuleSetName)

def Aesop.Frontend.RuleConfig.buildLocalRule (c : RuleConfig) : ElabM LocalRuleSetMember

def Aesop.Frontend.RuleConfig.toRuleFilter (c : RuleConfig) : ElabM (RuleSetNameFilter × RuleFilter)

def Aesop.Frontend.RuleConfig.validateForAdditionalRules {m : Type → Type} [Monad m] [Lean.MonadError m] (c : RuleConfig) (defaultRuleSet : RuleSetName) : m RuleConfig

def Aesop.Frontend.RuleExpr.toRuleConfigs {m : Type → Type} [Monad m] [Lean.MonadError m] (e : RuleExpr) (init : RuleConfig) : m (Array RuleConfig)

def Aesop.Frontend.RuleExpr.toAdditionalRules {m : Type → Type} [Monad m] [Lean.MonadError m] (e : RuleExpr) (init : RuleConfig) (defaultRuleSet : RuleSetName) : m (Array RuleConfig)

def Aesop.Frontend.RuleExpr.toAdditionalGlobalRules {m : Type → Type} [Monad m] [Lean.MonadError m] (decl? : Option Lean.Name) (e : RuleExpr) : m (Array RuleConfig)

def Aesop.Frontend.RuleExpr.buildAdditionalGlobalRules (decl? : Option Lean.Name) (e : RuleExpr) : Lean.Elab.TermElabM (Array (GlobalRuleSetMember × Array RuleSetName))

def Aesop.Frontend.RuleExpr.toAdditionalLocalRules (e : RuleExpr) : Lean.MetaM (Array RuleConfig)

def Aesop.Frontend.RuleExpr.buildAdditionalLocalRules (goal : Lean.MVarId) (e : RuleExpr) : Lean.Elab.TermElabM (Array LocalRuleSetMember)

def Aesop.Frontend.RuleExpr.toRuleFilters (e : RuleExpr) : ElabM (Array (RuleSetNameFilter × RuleFilter))

def Aesop.Frontend.RuleExpr.toGlobalRuleFilters (e : RuleExpr) : Lean.Elab.TermElabM (Array (RuleSetNameFilter × RuleFilter))

def Aesop.Frontend.RuleExpr.toLocalRuleFilters (e : RuleExpr) : ElabM (Array RuleFilter)