inductive Aesop.RuleBuilderKind : Type

• global: Lean.Name → Aesop.RuleBuilderKind
• local: Lean.Name → Lean.MVarId → Aesop.RuleBuilderKind

def Aesop.RuleBuilderKind.toRuleIdent : Aesop.RuleBuilderKind → Aesop.RuleIdent

Equations

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

structure Aesop.RuleBuilderInput : Type

• phase : Aesop.PhaseName
• kind : Aesop.RuleBuilderKind

structure Aesop.RegularRuleBuilderResult : Type

• builder : Aesop.BuilderName
• tac : Aesop.RuleTacDescr
• indexingMode : Aesop.IndexingMode

instance Aesop.instInhabitedRegularRuleBuilderResult : Inhabited Aesop.RegularRuleBuilderResult

Equations

• Aesop.instInhabitedRegularRuleBuilderResult = { default := { builder := default, tac := default, indexingMode := default } }

inductive Aesop.RuleBuilderResult : Type

• regular: Aesop.RegularRuleBuilderResult → Aesop.RuleBuilderResult
• globalSimp: Array Lean.Meta.SimpEntry → Aesop.RuleBuilderResult
• localSimp: Lean.Name → Aesop.RuleBuilderResult
• unfold: Aesop.UnfoldRule → Aesop.RuleBuilderResult

instance Aesop.instInhabitedRuleBuilderResult : Inhabited Aesop.RuleBuilderResult

Equations

• Aesop.instInhabitedRuleBuilderResult = { default := Aesop.RuleBuilderResult.regular default }

inductive Aesop.RuleBuilderOutput : Type

• global: Aesop.RuleBuilderResult → Aesop.RuleBuilderOutput
• local: Lean.MVarId → Aesop.RuleBuilderResult → Aesop.RuleBuilderOutput

@[inline, reducible]

abbrev Aesop.RuleBuilder : Type

Invariant: if the RuleBuilderInput contains a RuleBuilderKind.local, then the builder returns a RuleBuilderOutput.local, and similar for RuleBuilderKind.global.

Equations

• Aesop.RuleBuilder = (Aesop.RuleBuilderInput → Lean.MetaM Aesop.RuleBuilderOutput)

def Aesop.RuleBuilder.checkConstIsInductive (builderName : Aesop.BuilderName) (decl : Lean.Name) : Lean.MetaM Lean.InductiveVal

Equations

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

def Aesop.RuleBuilder.ofGlobalRuleBuilder (name : Aesop.BuilderName) (globalBuilder : Aesop.PhaseName → Lean.Name → Lean.MetaM Aesop.RuleBuilderResult) : Aesop.RuleBuilder

Equations

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

structure Aesop.RegularBuilderOptions : Type

• indexingMode? : Option Aesop.IndexingMode

instance Aesop.instInhabitedRegularBuilderOptions : Inhabited Aesop.RegularBuilderOptions

Equations

• Aesop.instInhabitedRegularBuilderOptions = { default := { indexingMode? := default } }

def Aesop.RegularBuilderOptions.default : Aesop.RegularBuilderOptions

Equations

• Aesop.RegularBuilderOptions.default = { indexingMode? := none }

def Aesop.RegularBuilderOptions.getIndexingModeM {m : Type → Type u_1} [Monad m] (dflt : m Aesop.IndexingMode) (opts : Aesop.RegularBuilderOptions) : m Aesop.IndexingMode

Equations

• Aesop.RegularBuilderOptions.getIndexingModeM dflt opts = match opts.indexingMode? with | none => dflt | some imode => pure imode