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.Fix
Lean.Elab.PreDefinition.WF.FloatRecApp
Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.PreDefinition.WF.PackMutual
Lean.Elab.PreDefinition.WF.Preprocess
Lean.Elab.PreDefinition.WF.Rel
Lean.Elab.PreDefinition.WF.Unfold
Imported by
Lean
.
Elab
.
wfRecursion
source
def
Lean
.
Elab
.
wfRecursion
(
preDefs
:
Array
PreDefinition
)
(
termMeasure?s
:
Array
(
Option
TerminationMeasure
)
)
:
TermElabM
Unit
Equations
Instances For