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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
inductive Aesop.Frontend.Priority :
Type

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

Instances For

source
instance Aesop.Frontend.instInhabitedPriority :
Inhabited Priority
Equations

- Aesop.Frontend.instInhabitedPriority = { default := Aesop.Frontend.instInhabitedPriority.default }

source
def Aesop.Frontend.instInhabitedPriority.default :
Priority
Equations

- Aesop.Frontend.instInhabitedPriority.default = Aesop.Frontend.Priority.int default

Instances For

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

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

Instances For

source
instance Aesop.Frontend.Priority.instToString :
ToString Priority
Equations

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

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

- (Aesop.Frontend.Priority.int i).toInt? = some i
- x✝.toInt? = none

Instances For

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

- (Aesop.Frontend.Priority.percent p).toPercent? = some p
- x✝.toPercent? = none

Instances For

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

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

Instances For

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

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

Instances For

source
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)

Instances For

source
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)

Instances For

source
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)

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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)

Instances For

source
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)

Instances For

source
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)

Instances For

source
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)

Instances For

source
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)

Instances For

source
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)

Instances For

source
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)

Instances For

source
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)

Instances For

source
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)

Instances For

source
inductive Aesop.Frontend.DBuilderName :
Type

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

Instances For

source
instance Aesop.Frontend.instInhabitedDBuilderName :
Inhabited DBuilderName
Equations

- Aesop.Frontend.instInhabitedDBuilderName = { default := Aesop.Frontend.instInhabitedDBuilderName.default }

source
def Aesop.Frontend.instInhabitedDBuilderName.default :
DBuilderName
Equations

- Aesop.Frontend.instInhabitedDBuilderName.default = Aesop.Frontend.DBuilderName.regular default

Instances For

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

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

Instances For

source
instance Aesop.Frontend.DBuilderName.instToString :
ToString DBuilderName
Equations

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

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

- (Aesop.Frontend.DBuilderName.regular b).toBuilderName? = some b
- x✝.toBuilderName? = none

Instances For

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

- (Aesop.Frontend.DBuilderName.regular Aesop.BuilderName.apply).toRuleBuilder = Aesop.RuleBuilder.apply
- (Aesop.Frontend.DBuilderName.regular Aesop.BuilderName.cases).toRuleBuilder = Aesop.RuleBuilder.cases
- (Aesop.Frontend.DBuilderName.regular Aesop.BuilderName.constructors).toRuleBuilder = Aesop.RuleBuilder.constructors
- (Aesop.Frontend.DBuilderName.regular Aesop.BuilderName.destruct).toRuleBuilder = Aesop.RuleBuilder.forward true
- (Aesop.Frontend.DBuilderName.regular Aesop.BuilderName.forward).toRuleBuilder = Aesop.RuleBuilder.forward false
- (Aesop.Frontend.DBuilderName.regular Aesop.BuilderName.simp).toRuleBuilder = Aesop.RuleBuilder.simp
- (Aesop.Frontend.DBuilderName.regular Aesop.BuilderName.tactic).toRuleBuilder = Aesop.RuleBuilder.tactic
- (Aesop.Frontend.DBuilderName.regular Aesop.BuilderName.unfold).toRuleBuilder = Aesop.RuleBuilder.unfold
- Aesop.Frontend.DBuilderName.default.toRuleBuilder = Aesop.RuleBuilder.default

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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)

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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.

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

- Aesop.Frontend.RuleSetName.elab stx = stx.getId.eraseMacroScopes

Instances For

source
structure Aesop.Frontend.RuleSets :
Type

- ruleSets : Array RuleSetName

Instances For

source
def Aesop.Frontend.instInhabitedRuleSets.default :
RuleSets
Equations

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

Instances For

source
instance Aesop.Frontend.instInhabitedRuleSets :
Inhabited RuleSets
Equations

- Aesop.Frontend.instInhabitedRuleSets = { default := Aesop.Frontend.instInhabitedRuleSets.default }

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

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

Instances For

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

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

Instances For

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

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

Instances For

source
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)

Instances For

source
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)

Instances For

source
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_name 0)

Instances For

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

- Aesop.Frontend.Parser.feature__3 = Lean.ParserDescr.node `Aesop.Frontend.Parser.feature__3 1022 (Lean.ParserDescr.cat `Aesop.builder_option 0)

Instances For

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

- Aesop.Frontend.Parser.feature__4 = Lean.ParserDescr.node `Aesop.Frontend.Parser.feature__4 1022 Aesop.Frontend.Parser.ruleSetsFeature

Instances For

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

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

Instances For

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

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

Instances For

source
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

Instances For

source
def Aesop.Frontend.instInhabitedFeature.default :
Feature
Equations

- Aesop.Frontend.instInhabitedFeature.default = Aesop.Frontend.Feature.phase default

Instances For

source
instance Aesop.Frontend.instInhabitedFeature :
Inhabited Feature
Equations

- Aesop.Frontend.instInhabitedFeature = { default := Aesop.Frontend.instInhabitedFeature.default }

source
partial def Aesop.Frontend.Feature.elab (stx : Lean.Syntax) :
ElabM Feature
source
def Lean.Parser.Category.Aesop.rule_expr :
Category
Equations

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

Instances For

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

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

Instances For

source
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)

Instances For

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

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

Instances For

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

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

Instances For

source
inductive Aesop.Frontend.RuleExpr :
Type

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

Instances For

source
instance Aesop.Frontend.instInhabitedRuleExpr :
Inhabited RuleExpr
Equations

- Aesop.Frontend.instInhabitedRuleExpr = { default := Aesop.Frontend.instInhabitedRuleExpr.default }

source
def Aesop.Frontend.instInhabitedRuleExpr.default :
RuleExpr
Equations

- Aesop.Frontend.instInhabitedRuleExpr.default = Aesop.Frontend.RuleExpr.node default default

Instances For

source
partial def Aesop.Frontend.RuleExpr.elab (stx : Lean.Syntax) :
ElabM RuleExpr
source
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 σ)
Equations

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

Instances For

source
structure Aesop.Frontend.RuleConfig :
Type

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

- c.getTerm = match c.term? with | some term => pure term | x => Lean.throwError (Lean.toMessageData "missing rule")

Instances For

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

- c.getPhase = match c.phase? with | some phase => pure phase | x => Lean.throwError (Lean.toMessageData "missing phase (norm/safe/unsafe)")

Instances For

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

- c.getBuilder = match c.builder? with | some builder => pure builder | x => Lean.throwError (Lean.toMessageData "missing rule builder (apply, forward, simp, ...)")

Instances For

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

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

Instances For

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

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

Instances For

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

- c.buildRule = do let builder ← c.getBuilder let builderInput ← liftM c.getRuleBuilderInput let ruleSetMember ← builder.toRuleBuilder builderInput pure (ruleSetMember, c.ruleSets.ruleSets)

Instances For

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

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

Instances For

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

- c.buildLocalRule = (fun (x : Aesop.LocalRuleSetMember × Array Aesop.RuleSetName) => x.fst) <$> c.buildRule

Instances For

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

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

Instances For

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

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

Instances For

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

- e.toRuleConfigs init = Aesop.Frontend.RuleExpr.foldBranchesM (fun (c : Aesop.Frontend.RuleConfig) (feature : Aesop.Frontend.Feature) => c.addFeature feature) init e

Instances For

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

- e.toAdditionalRules init defaultRuleSet = do let cs ← e.toRuleConfigs init Array.mapM (fun (x : Aesop.Frontend.RuleConfig) => x.validateForAdditionalRules defaultRuleSet) cs

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

- e.toGlobalRuleFilters = do let __do_lift ← liftM Aesop.ElabM.Context.forGlobalErasing Aesop.ElabM.run __do_lift e.toRuleFilters

Instances For

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

- e.toLocalRuleFilters = do let __do_lift ← e.toRuleFilters pure (Array.map (fun (x : Aesop.RuleSetNameFilter × Aesop.RuleFilter) => x.snd) __do_lift)

Instances For