HepLean Documentation
Lean
.
Meta
.
Constructions
.
RecOn
Search
Google site search
return to top
source
Imports
Lean.AddDecl
Lean.AuxRecursor
Lean.Meta.CompletionName
Lean.Meta.InferType
Imported by
mkRecOn
source
def
mkRecOn
(n :
Lake.Name
)
:
Lean.MetaM
Unit
Equations
One or more equations did not get rendered due to their size.
Instances For