Documentation
Lean
.
Meta
.
Constructions
.
RecOn
Search
return to top
source
Imports
Lean.AddDecl
Lean.AuxRecursor
Lean.Meta.CompletionName
Lean.Meta.InferType
Imported by
mkRecOn
source
def
mkRecOn
(
n
:
Lean.Name
)
:
Lean.MetaM
Unit
Equations
Instances For