Documentation

Aesop.RuleTac.RuleTerm

inductive Aesop.RuleTerm :

const (decl : Lean.Name) : RuleTerm
term (term : Lean.Term) : RuleTerm

Instances For

instance Aesop.instInhabitedRuleTerm :

Inhabited RuleTerm

Equations

Aesop.instInhabitedRuleTerm = { default := Aesop.RuleTerm.const default }

instance Aesop.instToMessageDataRuleTerm :

Lean.ToMessageData RuleTerm

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

Instances For

instance Aesop.instInhabitedElabRuleTerm :

Inhabited ElabRuleTerm

Equations

Aesop.instInhabitedElabRuleTerm = { default := Aesop.ElabRuleTerm.const default }

instance Aesop.ElabRuleTerm.instToMessageData :

Lean.ToMessageData ElabRuleTerm

Equations

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

def Aesop.ElabRuleTerm.expr :

ElabRuleTerm → Lean.MetaM Lean.Expr

Equations

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

def Aesop.ElabRuleTerm.scope :

ElabRuleTerm → ScopeName

Equations

(Aesop.ElabRuleTerm.const decl).scope = Aesop.ScopeName.global
(Aesop.ElabRuleTerm.term tm expr).scope = Aesop.ScopeName.local

def Aesop.ElabRuleTerm.name :

ElabRuleTerm → Lean.MetaM Lean.Name

Equations

(Aesop.ElabRuleTerm.const decl).name = pure decl
(Aesop.ElabRuleTerm.term tm expr).name = Aesop.getRuleNameForExpr expr

def Aesop.ElabRuleTerm.toRuleTerm :

ElabRuleTerm → RuleTerm

Equations

(Aesop.ElabRuleTerm.const decl).toRuleTerm = Aesop.RuleTerm.const decl
(Aesop.ElabRuleTerm.term tm expr).toRuleTerm = Aesop.RuleTerm.term tm

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