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 Lean.Term
• 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.ExtraRuleBuilderInput : Type

• safe: Int → Aesop.Safety → Aesop.ExtraRuleBuilderInput
• norm: Int → Aesop.ExtraRuleBuilderInput
• unsafe: Aesop.Percent → Aesop.ExtraRuleBuilderInput

instance Aesop.instInhabitedExtraRuleBuilderInput : Inhabited Aesop.ExtraRuleBuilderInput

Equations

• Aesop.instInhabitedExtraRuleBuilderInput = { default := Aesop.ExtraRuleBuilderInput.safe default default }

def Aesop.ExtraRuleBuilderInput.phase : Aesop.ExtraRuleBuilderInput → Aesop.PhaseName

Equations

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

structure Aesop.RuleBuilderInput : Type

• term : Lean.Term
• options : Aesop.RuleBuilderOptions
• extra : Aesop.ExtraRuleBuilderInput

instance Aesop.instInhabitedRuleBuilderInput : Inhabited Aesop.RuleBuilderInput

Equations

• Aesop.instInhabitedRuleBuilderInput = { default := { term := default, options := default, extra := default } }

def Aesop.RuleBuilderInput.phase (input : Aesop.RuleBuilderInput) : Aesop.PhaseName

Equations

• Aesop.RuleBuilderInput.phase input = Aesop.ExtraRuleBuilderInput.phase input.extra

def Aesop.RuleBuilderInput.toRule (builder : Aesop.BuilderName) (name : Lean.Name) (scope : Aesop.ScopeName) (tac : Aesop.RuleTacDescr) (indexingMode : Aesop.IndexingMode) (pattern? : Option Aesop.RulePattern) (input : Aesop.RuleBuilderInput) : Aesop.BaseRuleSetMember

Equations

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

@[inline, reducible]

abbrev Aesop.RuleBuilder : Type

Equations

• Aesop.RuleBuilder = (Aesop.RuleBuilderInput → Aesop.ElabM Aesop.LocalRuleSetMember)

def Aesop.elabGlobalRuleIdent (builderName : Aesop.BuilderName) (term : Lean.Term) : Lean.Elab.TermElabM Lean.Name

Equations

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

def Aesop.elabInductiveRuleIdent (builderName : Aesop.BuilderName) (term : Lean.Term) : Lean.Elab.TermElabM Lean.InductiveVal

Equations

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