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.instEmptyCollection : EmptyCollection Aesop.RuleBuilderOptions

Equations

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

structure Aesop.CoreRuleBuilderOutput : Type

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

inductive Aesop.PhaseSpec : Type

• safe: Aesop.SafeRuleInfo → Aesop.PhaseSpec
• norm: Aesop.NormRuleInfo → Aesop.PhaseSpec
• unsafe: Aesop.UnsafeRuleInfo → Aesop.PhaseSpec

instance Aesop.instInhabitedPhaseSpec : Inhabited Aesop.PhaseSpec

Equations

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

def Aesop.PhaseSpec.phase : Aesop.PhaseSpec → Aesop.PhaseName

Equations

• x.phase = match x with | Aesop.PhaseSpec.safe info => Aesop.PhaseName.safe | Aesop.PhaseSpec.unsafe info => Aesop.PhaseName.unsafe | Aesop.PhaseSpec.norm info => Aesop.PhaseName.norm

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

Equations

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

structure Aesop.RuleBuilderInput : Type

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

instance Aesop.instInhabitedRuleBuilderInput : Inhabited Aesop.RuleBuilderInput

Equations

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

def Aesop.RuleBuilderInput.phaseName (input : Aesop.RuleBuilderInput) : Aesop.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 : 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.

inductive Aesop.ElabRuleTerm : Type

• const: Lean.Name → Aesop.ElabRuleTerm
• term: Lean.Term → Lean.Expr → Aesop.ElabRuleTerm

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

Equations

• x.expr = match x with | Aesop.ElabRuleTerm.const decl => Lean.Meta.mkConstWithFreshMVarLevels decl | Aesop.ElabRuleTerm.term term e => pure e

def Aesop.ElabRuleTerm.scope : Aesop.ElabRuleTerm → Aesop.ScopeName

Equations

• x.scope = match x with | Aesop.ElabRuleTerm.const decl => Aesop.ScopeName.global | Aesop.ElabRuleTerm.term term expr => Aesop.ScopeName.local

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

Equations

• x.name = match x with | Aesop.ElabRuleTerm.const decl => pure decl | Aesop.ElabRuleTerm.term term e => Aesop.getRuleNameForExpr e

def Aesop.ElabRuleTerm.toRuleTerm : Aesop.ElabRuleTerm → Aesop.RuleTerm

Equations

• x.toRuleTerm = match x with | Aesop.ElabRuleTerm.const decl => Aesop.RuleTerm.const decl | Aesop.ElabRuleTerm.term t expr => Aesop.RuleTerm.term t

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

Equations

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