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 Aesop.instInhabitedRuleBuilderOptions : Inhabited RuleBuilderOptions

def Aesop.RuleBuilderOptions.default : RuleBuilderOptions

instance Aesop.RuleBuilderOptions.instEmptyCollection : EmptyCollection RuleBuilderOptions

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 Aesop.instInhabitedPhaseSpec : Inhabited PhaseSpec

def Aesop.PhaseSpec.phase : PhaseSpec → PhaseName

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

structure Aesop.RuleBuilderInput : Type

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

instance Aesop.instInhabitedRuleBuilderInput : Inhabited RuleBuilderInput

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

@[reducible, inline]

abbrev Aesop.RuleBuilder : Type

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

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