inductive Aesop.RuleTerm : Type

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

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

• const (decl : Lean.Name) : ElabRuleTerm
• term (term : Lean.Term) (expr : Lean.Expr) : ElabRuleTerm

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

Equations

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