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

Equations

• Lean.Parser.Category.Aesop.priority = { }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

inductive Aesop.Frontend.Priority : Type

• int: Int → Aesop.Frontend.Priority
• percent: Aesop.Percent → Aesop.Frontend.Priority

instance Aesop.Frontend.instInhabitedPriority : Inhabited Aesop.Frontend.Priority

Equations

• Aesop.Frontend.instInhabitedPriority = { default := Aesop.Frontend.Priority.int default }

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

Equations

• One or more equations did not get rendered due to their size.

instance Aesop.Frontend.Priority.instToStringPriority : ToString Aesop.Frontend.Priority

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.Frontend.Priority.toInt? x = match x with | Aesop.Frontend.Priority.int i => some i | x => none

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

Equations

• Aesop.Frontend.Priority.toPercent? x = match x with | Aesop.Frontend.Priority.percent p => some p | x => none

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

Equations

• Lean.Parser.Category.Aesop.phase = { }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.Frontend.Parser.phaseSafe = Lean.ParserDescr.node `Aesop.Frontend.Parser.phaseSafe 1024 (Lean.ParserDescr.nonReservedSymbol "safe" false)

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

Equations

• Aesop.Frontend.Parser.phaseNorm = Lean.ParserDescr.node `Aesop.Frontend.Parser.phaseNorm 1024 (Lean.ParserDescr.nonReservedSymbol "norm" false)

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

Equations

• Aesop.Frontend.Parser.phaseUnsafe = Lean.ParserDescr.node `Aesop.Frontend.Parser.phaseUnsafe 1024 (Lean.ParserDescr.nonReservedSymbol "unsafe" false)

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.Aesop.bool_lit : Lean.Parser.Category

Equations

• Lean.Parser.Category.Aesop.bool_lit = { }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.Frontend.Parser.bool_litTrue = Lean.ParserDescr.node `Aesop.Frontend.Parser.bool_litTrue 1024 (Lean.ParserDescr.nonReservedSymbol "true" false)

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

Equations

• Aesop.Frontend.Parser.bool_litFalse = Lean.ParserDescr.node `Aesop.Frontend.Parser.bool_litFalse 1024 (Lean.ParserDescr.nonReservedSymbol "false" false)

def Aesop.Frontend.elabBoolLit (stx : Lean.Syntax) : Aesop.Frontend.ElabM Bool

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.Category.Aesop.builder_name = { }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.Frontend.Parser.builder_nameApply = Lean.ParserDescr.node `Aesop.Frontend.Parser.builder_nameApply 1024 (Lean.ParserDescr.nonReservedSymbol "apply" false)

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

Equations

• Aesop.Frontend.Parser.builder_nameSimp = Lean.ParserDescr.node `Aesop.Frontend.Parser.builder_nameSimp 1024 (Lean.ParserDescr.nonReservedSymbol "simp" false)

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

Equations

• Aesop.Frontend.Parser.builder_nameUnfold = Lean.ParserDescr.node `Aesop.Frontend.Parser.builder_nameUnfold 1024 (Lean.ParserDescr.nonReservedSymbol "unfold" false)

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

Equations

• Aesop.Frontend.Parser.builder_nameTactic = Lean.ParserDescr.node `Aesop.Frontend.Parser.builder_nameTactic 1024 (Lean.ParserDescr.nonReservedSymbol "tactic" false)

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

Equations

• Aesop.Frontend.Parser.builder_nameConstructors = Lean.ParserDescr.node `Aesop.Frontend.Parser.builder_nameConstructors 1024 (Lean.ParserDescr.nonReservedSymbol "constructors" false)

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

Equations

• Aesop.Frontend.Parser.builder_nameForward = Lean.ParserDescr.node `Aesop.Frontend.Parser.builder_nameForward 1024 (Lean.ParserDescr.nonReservedSymbol "forward" false)

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

Equations

• Aesop.Frontend.Parser.builder_nameDestruct = Lean.ParserDescr.node `Aesop.Frontend.Parser.builder_nameDestruct 1024 (Lean.ParserDescr.nonReservedSymbol "destruct" false)

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

Equations

• Aesop.Frontend.Parser.builder_nameCases = Lean.ParserDescr.node `Aesop.Frontend.Parser.builder_nameCases 1024 (Lean.ParserDescr.nonReservedSymbol "cases" false)

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

Equations

• Aesop.Frontend.Parser.builder_nameDefault = Lean.ParserDescr.node `Aesop.Frontend.Parser.builder_nameDefault 1024 (Lean.ParserDescr.nonReservedSymbol "default" false)

inductive Aesop.Frontend.DBuilderName : Type

• regular: Aesop.BuilderName → Aesop.Frontend.DBuilderName
• default: Aesop.Frontend.DBuilderName

instance Aesop.Frontend.instInhabitedDBuilderName : Inhabited Aesop.Frontend.DBuilderName

Equations

• Aesop.Frontend.instInhabitedDBuilderName = { default := Aesop.Frontend.DBuilderName.regular default }

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

Equations

• One or more equations did not get rendered due to their size.

instance Aesop.Frontend.DBuilderName.instToStringDBuilderName : ToString Aesop.Frontend.DBuilderName

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.Frontend.DBuilderName.toBuilderName? x = match x with | Aesop.Frontend.DBuilderName.regular b => some b | x => none

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

Equations

• Lean.Parser.Category.Aesop.indexing_mode = { }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.Frontend.Parser.indexing_modeUnindexed = Lean.ParserDescr.node `Aesop.Frontend.Parser.indexing_modeUnindexed 1024 (Lean.ParserDescr.nonReservedSymbol "unindexed " false)

def Aesop.Frontend.elabPattern (stx : Lean.Syntax) : Lean.Elab.TermElabM Lean.Expr

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.elabPattern.adjustCtx (old : Lean.Elab.Term.Context) : Lean.Elab.Term.Context

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.elabSingleIndexingMode.elabKeys {s : Bool} (stx : Lean.Syntax) : Aesop.Frontend.ElabM (Array (Lean.Meta.DiscrTree.Key s))

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.Frontend.IndexingMode.elab stxs = Aesop.IndexingMode.or <$> Array.mapM Aesop.Frontend.elabSingleIndexingMode stxs

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

Equations

• Aesop.Frontend.CasesPattern.elab stx = do let __do_lift ← Aesop.Frontend.elabPattern stx liftM (Lean.Meta.abstractMVars __do_lift)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.Category.Aesop.builder_option = { }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

inductive Aesop.Frontend.BuilderOption : Type

• immediate: Array Lean.Name → Aesop.Frontend.BuilderOption
• index: Aesop.IndexingMode → Aesop.Frontend.BuilderOption
• patterns: Array Aesop.CasesPattern → Aesop.Frontend.BuilderOption
• transparency: Lean.Meta.TransparencyMode → Bool → Aesop.Frontend.BuilderOption

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

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.BuilderOption.name : Aesop.Frontend.BuilderOption → String

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.BuilderOption.toCtorIdx : Aesop.Frontend.BuilderOption → Nat

Equations

• One or more equations did not get rendered due to their size.

structure Aesop.Frontend.BuilderOptions (σ : Type u_1) : Type u_1

• builderName : Aesop.Frontend.DBuilderName
• init : σ
• add : σ → Aesop.Frontend.BuilderOption → Option σ

def Aesop.Frontend.BuilderOptions.elab {α : Type} (bo : Aesop.Frontend.BuilderOptions α) (stx : Lean.Syntax) : Aesop.Frontend.ElabM α

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.BuilderOptions.none (builderName : Aesop.Frontend.DBuilderName) : Aesop.Frontend.BuilderOptions Unit

Equations

• Aesop.Frontend.BuilderOptions.none builderName = { builderName := builderName, init := (), add := fun x x => none }

def Aesop.Frontend.BuilderOptions.regular (builderName : Aesop.BuilderName) : Aesop.Frontend.BuilderOptions Aesop.RegularBuilderOptions

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.BuilderOptions.forward : Aesop.Frontend.BuilderOptions Aesop.ForwardBuilderOptions

Equations

• Aesop.Frontend.BuilderOptions.forward = Aesop.Frontend.BuilderOptions.forwardCore false

def Aesop.Frontend.BuilderOptions.destruct : Aesop.Frontend.BuilderOptions Aesop.ForwardBuilderOptions

Equations

• Aesop.Frontend.BuilderOptions.destruct = Aesop.Frontend.BuilderOptions.forwardCore true

def Aesop.Frontend.BuilderOptions.cases : Aesop.Frontend.BuilderOptions Aesop.CasesBuilderOptions

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.BuilderOptions.apply : Aesop.Frontend.BuilderOptions Aesop.ApplyBuilderOptions

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.BuilderOptions.constructors : Aesop.Frontend.BuilderOptions Aesop.ConstructorsBuilderOptions

Equations

• One or more equations did not get rendered due to their size.

def Lean.Parser.Category.Aesop.builder : Lean.Parser.Category

Equations

• Lean.Parser.Category.Aesop.builder = { }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.Frontend.Parser.builder_ = Lean.ParserDescr.node `Aesop.Frontend.Parser.builder_ 1022 (Lean.ParserDescr.cat `Aesop.builder_name 0)

def Aesop.Frontend.Parser.«builder(__)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

inductive Aesop.Frontend.Builder : Type

• apply: Aesop.ApplyBuilderOptions → Aesop.Frontend.Builder
• simp: Aesop.Frontend.Builder
• unfold: Aesop.Frontend.Builder
• tactic: Aesop.RegularBuilderOptions → Aesop.Frontend.Builder
• constructors: Aesop.ConstructorsBuilderOptions → Aesop.Frontend.Builder
• forward: Aesop.ForwardBuilderOptions → Aesop.Frontend.Builder
• cases: Aesop.CasesBuilderOptions → Aesop.Frontend.Builder
• default: Aesop.Frontend.Builder

instance Aesop.Frontend.instInhabitedBuilder : Inhabited Aesop.Frontend.Builder

Equations

• Aesop.Frontend.instInhabitedBuilder = { default := Aesop.Frontend.Builder.apply default }

def Aesop.Frontend.Builder.elabOptions (b : Aesop.Frontend.DBuilderName) (opts : Lean.Syntax) : Aesop.Frontend.ElabM Aesop.Frontend.Builder

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.Builder.elabOptions.checkNoOptions (b : Aesop.Frontend.DBuilderName) (opts : Lean.Syntax) : Aesop.Frontend.ElabM Unit

Equations

• Aesop.Frontend.Builder.elabOptions.checkNoOptions b opts = Aesop.Frontend.BuilderOptions.elab (Aesop.Frontend.BuilderOptions.none b) opts

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.Builder.toDBuilderName : Aesop.Frontend.Builder → Aesop.Frontend.DBuilderName

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.Frontend.RuleSetName.elab stx = Lean.Name.eraseMacroScopes (Lean.Syntax.getId stx)

structure Aesop.Frontend.RuleSets : Type

• ruleSets : Array Aesop.RuleSetName

instance Aesop.Frontend.instInhabitedRuleSets : Inhabited Aesop.Frontend.RuleSets

Equations

• Aesop.Frontend.instInhabitedRuleSets = { default := { ruleSets := default } }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Parser.Category.Aesop.feature = { }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.Frontend.Parser.feature_ = Lean.ParserDescr.node `Aesop.Frontend.Parser.feature_ 1022 (Lean.ParserDescr.cat `Aesop.phase 0)

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

Equations

• Aesop.Frontend.Parser.feature__1 = Lean.ParserDescr.node `Aesop.Frontend.Parser.feature__1 1022 (Lean.ParserDescr.cat `Aesop.priority 0)

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

Equations

• Aesop.Frontend.Parser.feature__2 = Lean.ParserDescr.node `Aesop.Frontend.Parser.feature__2 1022 (Lean.ParserDescr.cat `Aesop.builder 0)

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

Equations

• Aesop.Frontend.Parser.feature__3 = Lean.ParserDescr.node `Aesop.Frontend.Parser.feature__3 1022 Aesop.Frontend.Parser.ruleSetsFeature

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

Equations

• Aesop.Frontend.Parser.featIdent = Lean.ParserDescr.node `Aesop.Frontend.Parser.featIdent 1022 (Lean.ParserDescr.const `ident)

inductive Aesop.Frontend.Feature : Type

• phase: Aesop.PhaseName → Aesop.Frontend.Feature
• priority: Aesop.Frontend.Priority → Aesop.Frontend.Feature
• builder: Aesop.Frontend.Builder → Aesop.Frontend.Feature
• ident: Aesop.RuleIdent → Aesop.Frontend.Feature
• ruleSets: Aesop.Frontend.RuleSets → Aesop.Frontend.Feature

instance Aesop.Frontend.instInhabitedFeature : Inhabited Aesop.Frontend.Feature

Equations

• Aesop.Frontend.instInhabitedFeature = { default := Aesop.Frontend.Feature.phase default }

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

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

Equations

• Lean.Parser.Category.Aesop.rule_expr = { }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Aesop.Frontend.Parser.rule_expr_ = Lean.ParserDescr.node `Aesop.Frontend.Parser.rule_expr_ 1022 (Lean.ParserDescr.cat `Aesop.feature 0)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

inductive Aesop.Frontend.RuleExpr : Type

• node: Aesop.Frontend.Feature → Array Aesop.Frontend.RuleExpr → Aesop.Frontend.RuleExpr

instance Aesop.Frontend.instInhabitedRuleExpr : Inhabited Aesop.Frontend.RuleExpr

Equations

• Aesop.Frontend.instInhabitedRuleExpr = { default := Aesop.Frontend.RuleExpr.node default default }

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

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

Equations

• Aesop.Frontend.RuleExpr.foldBranchesM f init e = Aesop.Frontend.RuleExpr.foldBranchesM.go f init #[] e

partial def Aesop.Frontend.RuleExpr.foldBranchesM.go {σ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] (f : σ → Aesop.Frontend.Feature → m σ) (c : σ) (acc : Array σ) : Aesop.Frontend.RuleExpr → m (Array σ)

structure Aesop.Frontend.RuleConfig (f : Type → Type) : Type

• ident : f Aesop.RuleIdent
• phase : f Aesop.PhaseName
• priority : f Aesop.Frontend.Priority
• builder : f Aesop.Frontend.Builder
• ruleSets : Aesop.Frontend.RuleSets

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.RuleConfig.buildLocalRule (c : Aesop.Frontend.RuleConfig Id) (goal : Lean.MVarId) : Lean.MetaM (Lean.MVarId × Aesop.RuleSetMember × Array Aesop.RuleSetName)

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.RuleConfig.buildLocalRule.runBuilder (c : Aesop.Frontend.RuleConfig Id) (goal : Lean.MVarId) (phase : Aesop.PhaseName) (b : Aesop.Frontend.Builder) : Lean.MetaM (Lean.MVarId × Aesop.RuleBuilderResult)

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.RuleConfig.buildLocalRule.runRegularBuilder (c : Aesop.Frontend.RuleConfig Id) (goal : Lean.MVarId) (phase : Aesop.PhaseName) (b : Aesop.Frontend.Builder) : Lean.MetaM (Lean.MVarId × Aesop.RegularRuleBuilderResult)

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.RuleConfig.buildGlobalRule (c : Aesop.Frontend.RuleConfig Id) : Lean.MetaM (Aesop.RuleSetMember × Array Aesop.RuleSetName)

Equations

• Aesop.Frontend.RuleConfig.buildGlobalRule c = Prod.snd <$> Aesop.Frontend.RuleConfig.buildLocalRule c { name := `_dummy }

def Aesop.Frontend.RuleConfig.toRuleNameFilter {m : Type → Type} [Monad m] [Lean.MonadError m] (c : Aesop.Frontend.RuleConfig Option) : m (Aesop.RuleSetNameFilter × Aesop.RuleNameFilter)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.RuleExpr.toAdditionalRules.go {m : Type → Type} [Monad m] [Lean.MonadError m] (r : Aesop.Frontend.RuleConfig Option) : Aesop.Frontend.Feature → m (Aesop.Frontend.RuleConfig Option)

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.RuleExpr.toAdditionalRules.getPhaseAndPriority {m : Type → Type} [Monad m] [Lean.MonadError m] (c : Aesop.Frontend.RuleConfig Option) : m (Aesop.PhaseName × Aesop.Frontend.Priority)

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.RuleExpr.toAdditionalRules.finish {m : Type → Type} [Monad m] [Lean.MonadError m] (defaultRuleSet : Aesop.RuleSetName) (c : Aesop.Frontend.RuleConfig Option) : m (Aesop.Frontend.RuleConfig Id)

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.RuleExpr.buildAdditionalGlobalRules (decl : Lean.Name) (e : Aesop.Frontend.RuleExpr) : Lean.MetaM (Array (Aesop.RuleSetMember × Array Aesop.RuleSetName))

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.RuleExpr.buildAdditionalLocalRules (goal : Lean.MVarId) (e : Aesop.Frontend.RuleExpr) : Lean.MetaM (Lean.MVarId × Array (Aesop.RuleSetMember × Array Aesop.RuleSetName))

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.RuleExpr.toRuleNameFilters {m : Type → Type} [Monad m] [Lean.MonadError m] (e : Aesop.Frontend.RuleExpr) : m (Array (Aesop.RuleSetNameFilter × Aesop.RuleNameFilter))

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.RuleExpr.toRuleNameFilters.go {m : Type → Type} [Monad m] [Lean.MonadError m] (r : Aesop.Frontend.RuleConfig Option) : Aesop.Frontend.Feature → m (Aesop.Frontend.RuleConfig Option)

Equations

• One or more equations did not get rendered due to their size.

def Aesop.Frontend.RuleExpr.toGlobalRuleNameFilters {m : Type → Type} [Monad m] [Lean.MonadError m] (e : Aesop.Frontend.RuleExpr) : m (Array (Aesop.RuleSetNameFilter × Aesop.RuleNameFilter))

Equations

• Aesop.Frontend.RuleExpr.toGlobalRuleNameFilters e = Aesop.Frontend.RuleExpr.toRuleNameFilters e

def Aesop.Frontend.RuleExpr.toLocalRuleNameFilters (goal : Lean.MVarId) (e : Aesop.Frontend.RuleExpr) : Lean.MetaM (Array (Aesop.RuleSetNameFilter × Aesop.RuleNameFilter))

Equations

• Aesop.Frontend.RuleExpr.toLocalRuleNameFilters goal e = Lean.MVarId.withContext goal (Aesop.Frontend.RuleExpr.toRuleNameFilters e)