Documentation

Aesop.Builder.Basic

structure Aesop.RuleBuilderOptions :

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.

Instances For

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 :

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

inductive Aesop.PhaseSpec :

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

Instances For

Aesop.instInhabitedPhaseSpec

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 :

Instances For

Aesop.instInhabitedRuleBuilderInput

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 :

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 :

const: Lean.Name → Aesop.ElabRuleTerm
term: Lean.Term → 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