structure Aesop.RuleBuilderOptions : Type

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

• immediatePremises? : Option (Array Lean.Name)
• indexingMode? : Option IndexingMode
• casesPatterns? : Option (Array 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_reducible]

instance Aesop.instInhabitedRuleBuilderOptions : Inhabited RuleBuilderOptions

Equations

• Aesop.instInhabitedRuleBuilderOptions = { default := Aesop.instInhabitedRuleBuilderOptions.default }

def Aesop.RuleBuilderOptions.default : RuleBuilderOptions

Equations

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

@[instance_reducible]

instance Aesop.RuleBuilderOptions.instEmptyCollection : EmptyCollection RuleBuilderOptions

Equations

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

structure Aesop.CoreRuleBuilderOutput : Type

• ruleExprName : Lean.Name
• builderName : BuilderName
• scopeName : ScopeName
• tac : RuleTacDescr
• indexingMode : IndexingMode
• pattern? : Option RulePattern

inductive Aesop.PhaseSpec : Type

• safe (info : SafeRuleInfo) : PhaseSpec
• norm (info : NormRuleInfo) : PhaseSpec
• unsafe (info : UnsafeRuleInfo) : PhaseSpec

@[instance_reducible]

instance Aesop.instInhabitedPhaseSpec : Inhabited PhaseSpec

Equations

• Aesop.instInhabitedPhaseSpec = { default := Aesop.instInhabitedPhaseSpec.default }

def Aesop.PhaseSpec.phase : PhaseSpec → PhaseName

Equations

• (Aesop.PhaseSpec.safe info).phase = Aesop.PhaseName.safe
• (Aesop.PhaseSpec.unsafe info).phase = Aesop.PhaseName.unsafe
• (Aesop.PhaseSpec.norm info).phase = Aesop.PhaseName.norm

def Aesop.PhaseSpec.toRule (phase : PhaseSpec) (ruleExprName : Lean.Name) (builder : BuilderName) (scope : ScopeName) (tac : RuleTacDescr) (indexingMode : IndexingMode) (pattern? : Option RulePattern) : BaseRuleSetMember

Equations

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

structure Aesop.RuleBuilderInput : Type

• term : Lean.Term
• options : RuleBuilderOptions
• phase : PhaseSpec

@[instance_reducible]

instance Aesop.instInhabitedRuleBuilderInput : Inhabited RuleBuilderInput

Equations

• Aesop.instInhabitedRuleBuilderInput = { default := Aesop.instInhabitedRuleBuilderInput.default }

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

Equations

• input.phaseName = input.phase.phase

@[reducible, inline]

abbrev Aesop.RuleBuilder : Type

Equations

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

def Aesop.elabGlobalRuleIdent (builderName : 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 : BuilderName) (term : Lean.Term) (md : Lean.Meta.TransparencyMode) : Lean.Elab.TermElabM (Lean.Name × Lean.InductiveVal)

Equations

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