Documentation
Lean
.
Meta
.
Constructions
.
BRecOn
Search
return to top
source
Imports
Lean.Meta.Basic
Lean.Meta.CompletionName
Lean.Meta.PProdN
Lean.Meta.Tactic.Cases
Lean.Meta.Tactic.Refl
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