structure Aesop.RuleBuilderOptions : Type

Options for the builders. Most options are only relevant for certain builders.

• immediatePremises? : Option (Array Lean.Name)
• indexingMode? : Option Aesop.IndexingMode
• casesPatterns? : Option (Array Aesop.CasesPattern)
• pattern? : Option Aesop.RulePattern
• transparency? : Option Lean.Meta.TransparencyMode

  The transparency used by the rule tactic.

• indexTransparency? : Option Lean.Meta.TransparencyMode

  The transparency used for indexing the rule. Currently, the rule is not indexed unless this is .reducible.

instance Aesop.instInhabitedRuleBuilderOptions : Inhabited Aesop.RuleBuilderOptions

Equations

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

def Aesop.RuleBuilderOptions.default : Aesop.RuleBuilderOptions

Equations

• Aesop.RuleBuilderOptions.default = { immediatePremises? := none, indexingMode? := none, casesPatterns? := none, pattern? := none, transparency? := none, indexTransparency? := none }

instance Aesop.RuleBuilderOptions.instEmptyCollectionRuleBuilderOptions : EmptyCollection Aesop.RuleBuilderOptions

Equations

• Aesop.RuleBuilderOptions.instEmptyCollectionRuleBuilderOptions = { emptyCollection := Aesop.RuleBuilderOptions.default }

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

Equations

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

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
• options : Aesop.RuleBuilderOptions

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 → Aesop.RuleBuilderOptions → Lean.MetaM Aesop.RuleBuilderResult) : Aesop.RuleBuilder

Equations

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