Documentation
Lean
.
Meta
.
Constructions
.
BRecOn
Search
return to top
source
Imports
Lean.AddDecl
Lean.AuxRecursor
Lean.Meta.CompletionName
Lean.Meta.InferType
Lean.Meta.PProdN
Imported by
Lean
.
mkBelow
Lean
.
mkBRecOn
source
def
Lean
.
mkBelow
(
indName
:
Name
)
:
MetaM
Unit
Equations
One or more equations did not get rendered due to their size.
Instances For
source
def
Lean
.
mkBRecOn
(
indName
:
Name
)
:
MetaM
Unit
Equations
One or more equations did not get rendered due to their size.
Instances For