Documentation
Aesop
.
Builder
.
Unfold
Search
Google site search
return to top
source
Imports
Init
Aesop.Builder.Basic
Imported by
Aesop
.
RuleBuilder
.
hasConst
Aesop
.
RuleBuilder
.
checkUnfoldableConst
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
.
unfold
:
Aesop.RuleBuilder
Equations
One or more equations did not get rendered due to their size.
Instances For