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 (info : Aesop.SafeRuleInfo) : Aesop.PhaseSpec
• norm (info : Aesop.NormRuleInfo) : Aesop.PhaseSpec
• unsafe (info : 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

• (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 : 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 (decl : Lean.Name) : Aesop.ElabRuleTerm
• term (term : Lean.Term) (expr : Lean.Expr) : Aesop.ElabRuleTerm

def Aesop.ElabRuleTerm.expr : Aesop.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 : Aesop.ElabRuleTerm → Aesop.ScopeName

Equations

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

def Aesop.ElabRuleTerm.name : Aesop.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 : Aesop.ElabRuleTerm → Aesop.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) : Aesop.ElabRuleTerm

Equations

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