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

Equations

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

def Aesop.RuleBuilderOptions.default : RuleBuilderOptions

Equations

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

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

Equations

• Aesop.instInhabitedPhaseSpec = { default := Aesop.PhaseSpec.safe 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 Aesop.instInhabitedRuleBuilderInput : Inhabited RuleBuilderInput

Equations

• Aesop.instInhabitedRuleBuilderInput = { default := { term := default, options := default, phase := 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) : Lean.Elab.TermElabM Lean.InductiveVal

Equations

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

inductive Aesop.ElabRuleTerm : Type

• const (decl : Lean.Name) : ElabRuleTerm
• term (term : Lean.Term) (expr : Lean.Expr) : ElabRuleTerm

def Aesop.ElabRuleTerm.expr : ElabRuleTerm → Lean.MetaM Lean.Expr

Equations

• (Aesop.ElabRuleTerm.const decl).expr = Lean.Meta.mkConstWithFreshMVarLevels decl
• (Aesop.ElabRuleTerm.term term e).expr = pure e

def Aesop.ElabRuleTerm.scope : ElabRuleTerm → ScopeName

Equations

• (Aesop.ElabRuleTerm.const decl).scope = Aesop.ScopeName.global
• (Aesop.ElabRuleTerm.term term e).scope = Aesop.ScopeName.local

def Aesop.ElabRuleTerm.name : ElabRuleTerm → Lean.MetaM Lean.Name

Equations

• (Aesop.ElabRuleTerm.const decl).name = pure decl
• (Aesop.ElabRuleTerm.term term e).name = Aesop.getRuleNameForExpr e

def Aesop.ElabRuleTerm.toRuleTerm : ElabRuleTerm → RuleTerm

Equations

• (Aesop.ElabRuleTerm.const decl).toRuleTerm = Aesop.RuleTerm.const decl
• (Aesop.ElabRuleTerm.term term e).toRuleTerm = Aesop.RuleTerm.term term

def Aesop.ElabRuleTerm.ofElaboratedTerm (tm : Lean.Term) (expr : Lean.Expr) : ElabRuleTerm

Equations

• Aesop.ElabRuleTerm.ofElaboratedTerm tm expr = match expr.constName? with | some decl => Aesop.ElabRuleTerm.const decl | x => Aesop.ElabRuleTerm.term tm expr