Documentation
Aesop
.
Rule
.
Basic
Search
return to top
source
Imports
Init
Aesop.Index.Basic
Aesop.Rule.Name
Aesop.RuleTac.Basic
Aesop.RuleTac.Descr
Imported by
Aesop
.
Rule
Aesop
.
instInhabitedRule
Aesop
.
Rule
.
instBEq
Aesop
.
Rule
.
instOrd
Aesop
.
Rule
.
instHashable
Aesop
.
Rule
.
compareByPriority
Aesop
.
Rule
.
compareByName
Aesop
.
Rule
.
compareByPriorityThenName
Aesop
.
Rule
.
map
Aesop
.
Rule
.
mapM
source
structure
Aesop
.
Rule
(
α
:
Type
)
:
Type
name :
RuleName
indexingMode :
IndexingMode
pattern? :
Option
RulePattern
extra :
α
tac :
RuleTacDescr
Instances For
source
instance
Aesop
.
instInhabitedRule
{
a✝
:
Type
}
[
Inhabited
a✝
]
:
Inhabited
(
Rule
a✝
)
Equations
source
instance
Aesop
.
Rule
.
instBEq
{
α
:
Type
}
:
BEq
(
Rule
α
)
Equations
source
instance
Aesop
.
Rule
.
instOrd
{
α
:
Type
}
:
Ord
(
Rule
α
)
Equations
source
instance
Aesop
.
Rule
.
instHashable
{
α
:
Type
}
:
Hashable
(
Rule
α
)
Equations
source
def
Aesop
.
Rule
.
compareByPriority
{
α
:
Type
}
[
Ord
α
]
(
r
s
:
Rule
α
)
:
Ordering
Equations
Instances For
source
def
Aesop
.
Rule
.
compareByName
{
α
:
Type
}
(
r
s
:
Rule
α
)
:
Ordering
Equations
Instances For
source
def
Aesop
.
Rule
.
compareByPriorityThenName
{
α
:
Type
}
[
Ord
α
]
(
r
s
:
Rule
α
)
:
Ordering
Equations
Instances For
source
@[inline]
def
Aesop
.
Rule
.
map
{
α
β
:
Type
}
(
f
:
α
→
β
)
(
r
:
Rule
α
)
:
Rule
β
Equations
Instances For
source
@[inline]
def
Aesop
.
Rule
.
mapM
{
m
:
Type
→
Type
u_1
}
{
α
β
:
Type
}
[
Monad
m
]
(
f
:
α
→
m
β
)
(
r
:
Rule
α
)
:
m
(
Rule
β
)
Equations
Instances For