inductive Aesop.RuleTerm : Type

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

def Aesop.instInhabitedRuleTerm.default : RuleTerm

@[implicit_reducible]

instance Aesop.instInhabitedRuleTerm : Inhabited RuleTerm

@[implicit_reducible]

instance Aesop.instToMessageDataRuleTerm : Lean.ToMessageData RuleTerm

inductive Aesop.ElabRuleTerm : Type

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

@[implicit_reducible]

instance Aesop.instInhabitedElabRuleTerm : Inhabited ElabRuleTerm

def Aesop.instInhabitedElabRuleTerm.default : ElabRuleTerm

@[implicit_reducible]

instance Aesop.ElabRuleTerm.instToMessageData : Lean.ToMessageData ElabRuleTerm

def Aesop.ElabRuleTerm.expr : ElabRuleTerm → Lean.MetaM Lean.Expr

def Aesop.ElabRuleTerm.scope : ElabRuleTerm → ScopeName

def Aesop.ElabRuleTerm.name : ElabRuleTerm → Lean.MetaM Lean.Name

def Aesop.ElabRuleTerm.toRuleTerm : ElabRuleTerm → RuleTerm

def Aesop.ElabRuleTerm.ofElaboratedTerm (tm : Lean.Term) (expr : Lean.Expr) : ElabRuleTerm