Documentation
Aesop
.
Builder
.
NormSimp
Search
return to top
source
Imports
Init
Aesop.Builder.Basic
Imported by
Aesop
.
PhaseSpec
.
getSimpPrio
Aesop
.
RuleBuilder
.
simpCore
Aesop
.
RuleBuilder
.
simp
source
def
Aesop
.
PhaseSpec
.
getSimpPrio
{
m
:
Type
→
Type
}
[
Monad
m
]
[
Lean.MonadError
m
]
:
PhaseSpec
→
m
Nat
Equations
Instances For
source
def
Aesop
.
RuleBuilder
.
simpCore
(
decl
:
Lean.Name
)
(
phase
:
PhaseSpec
)
:
Lean.MetaM
LocalRuleSetMember
Equations
Instances For
source
def
Aesop
.
RuleBuilder
.
simp
:
RuleBuilder
Equations
Instances For