Documentation
Aesop
.
Builder
.
Unfold
Search
return to top
source
Imports
Init
Aesop.Builder.Basic
Aesop.Util.Tactic.Unfold
Imported by
Aesop
.
RuleBuilder
.
hasConst
Aesop
.
RuleBuilder
.
checkUnfoldableConst
Aesop
.
RuleBuilder
.
unfoldCore
Aesop
.
RuleBuilder
.
unfold
source
def
Aesop
.
RuleBuilder
.
hasConst
(c :
Lean.Name
)
(e :
Lean.Expr
)
:
Bool
Equations
Aesop.RuleBuilder.hasConst
c
e
=
e
.
foldConsts
false
fun (
c'
:
Lean.Name
) (
acc
:
Bool
) =>
acc
||
c'
==
c
Instances For
source
def
Aesop
.
RuleBuilder
.
checkUnfoldableConst
(decl :
Lean.Name
)
:
Lean.MetaM
(
Option
Lean.Name
)
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Aesop
.
RuleBuilder
.
unfoldCore
(decl :
Lean.Name
)
:
Lean.MetaM
LocalRuleSetMember
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Aesop
.
RuleBuilder
.
unfold
:
RuleBuilder
Equations
Aesop.RuleBuilder.unfold
input
=
do let
decl
←
liftM
(
Aesop.elabGlobalRuleIdent
Aesop.BuilderName.unfold
input
.
term
)
liftM
(
Aesop.RuleBuilder.unfoldCore
decl
)
Instances For