Documentation
Lean
.
Elab
.
PreDefinition
.
PartialFixpoint
.
Induction
Search
return to top
source
Imports
Lean.Meta.Injective
Lean.Meta.PProdN
Init.Internal.Order.Basic
Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Imported by
← Mathematical handbook