Documentation
Lean
.
Elab
.
PreDefinition
.
WF
.
Main
Search
return to top
source
Imports
Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.Mutual
Lean.Elab.PreDefinition.TerminationMeasure
Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.PreDefinition.WF.Fix
Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.PreDefinition.WF.Ite
Lean.Elab.PreDefinition.WF.PackMutual
Lean.Elab.PreDefinition.WF.Preprocess
Lean.Elab.PreDefinition.WF.Rel
Imported by
Lean
.
Elab
.
wfRecursion
source
def
Lean
.
Elab
.
wfRecursion
(preDefs :
Array
PreDefinition
)
(termMeasure?s :
Array
(
Option
TerminationMeasure
)
)
:
TermElabM
Unit
Equations
One or more equations did not get rendered due to their size.
Instances For