Documentation
Aesop
.
RuleTac
.
RuleTerm
Search
return to top
source
Imports
Init
Aesop.Rule.Name
Imported by
Aesop
.
RuleTerm
Aesop
.
instInhabitedRuleTerm
Aesop
.
instToMessageDataRuleTerm
Aesop
.
ElabRuleTerm
Aesop
.
instInhabitedElabRuleTerm
Aesop
.
ElabRuleTerm
.
instToMessageData
Aesop
.
ElabRuleTerm
.
expr
Aesop
.
ElabRuleTerm
.
scope
Aesop
.
ElabRuleTerm
.
name
Aesop
.
ElabRuleTerm
.
toRuleTerm
Aesop
.
ElabRuleTerm
.
ofElaboratedTerm
source
inductive
Aesop
.
RuleTerm
:
Type
const
(
decl
:
Lean.Name
)
:
RuleTerm
term
(
term
:
Lean.Term
)
:
RuleTerm
Instances For
source
instance
Aesop
.
instInhabitedRuleTerm
:
Inhabited
RuleTerm
Equations
source
instance
Aesop
.
instToMessageDataRuleTerm
:
Lean.ToMessageData
RuleTerm
Equations
source
inductive
Aesop
.
ElabRuleTerm
:
Type
const
(
decl
:
Lean.Name
)
:
ElabRuleTerm
term
(
term
:
Lean.Term
)
(
expr
:
Lean.Expr
)
:
ElabRuleTerm
Instances For
source
instance
Aesop
.
instInhabitedElabRuleTerm
:
Inhabited
ElabRuleTerm
Equations
source
instance
Aesop
.
ElabRuleTerm
.
instToMessageData
:
Lean.ToMessageData
ElabRuleTerm
Equations
source
def
Aesop
.
ElabRuleTerm
.
expr
:
ElabRuleTerm
→
Lean.MetaM
Lean.Expr
Equations
Instances For
source
def
Aesop
.
ElabRuleTerm
.
scope
:
ElabRuleTerm
→
ScopeName
Equations
Instances For
source
def
Aesop
.
ElabRuleTerm
.
name
:
ElabRuleTerm
→
Lean.MetaM
Lean.Name
Equations
Instances For
source
def
Aesop
.
ElabRuleTerm
.
toRuleTerm
:
ElabRuleTerm
→
RuleTerm
Equations
Instances For
source
def
Aesop
.
ElabRuleTerm
.
ofElaboratedTerm
(
tm
:
Lean.Term
)
(
expr
:
Lean.Expr
)
:
ElabRuleTerm
Equations
Instances For