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 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.

Instances For

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 :

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

inductive Aesop.PhaseSpec :

safe (info : SafeRuleInfo) : PhaseSpec
norm (info : NormRuleInfo) : PhaseSpec
unsafe (info : UnsafeRuleInfo) : PhaseSpec

Instances For

Aesop.instInhabitedPhaseSpec

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 :

term : Lean.Term
options : RuleBuilderOptions
phase : PhaseSpec

Instances For

Aesop.instInhabitedRuleBuilderInput

instance Aesop.instInhabitedRuleBuilderInput :

Inhabited RuleBuilderInput

Equations

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

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

Equations

input.phaseName = input.phase.phase

@[reducible, inline]

abbrev Aesop.RuleBuilder :

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 :

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) :

Equations

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