Documentation
Lean
.
Elab
.
PreDefinition
.
PartialFixpoint
.
Main
Search
return to top
source
Imports
Lean.Meta.Order
Lean.Meta.PProdN
Init.Internal.Order.Basic
Lean.Elab.PreDefinition.MkInhabitant
Lean.Elab.PreDefinition.Mutual
Lean.Elab.Tactic.Monotonicity
Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Imported by
Lean
.
Elab
.
partialFixpoint
source
def
Lean
.
Elab
.
partialFixpoint
(
preDefs
:
Array
PreDefinition
)
:
TermElabM
Unit
Equations
Instances For