Documentation
Lean
.
Elab
.
PreDefinition
.
WF
.
Unfold
Search
return to top
source
Imports
Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.Eqns
Imported by
Lean
.
Elab
.
WF
.
mkUnfoldEq
source
def
Lean
.
Elab
.
WF
.
mkUnfoldEq
(
preDef
:
PreDefinition
)
(
unaryPreDefName
:
Name
)
(
wfPreprocessProof
:
Meta.Simp.Result
)
:
MetaM
Unit
Equations
One or more equations did not get rendered due to their size.
Instances For