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
.
mkIBelow
Lean
.
mkBRecOnOrBInductionOn
Lean
.
mkBRecOn
Lean
.
mkBInductionOn
source
def
Lean
.
mkBelow
(
declName
:
Name
)
:
MetaM
Unit
Equations
Instances For
source
def
Lean
.
mkIBelow
(
declName
:
Name
)
:
MetaM
Unit
Equations
Instances For
source
def
Lean
.
mkBRecOnOrBInductionOn
(
indName
:
Name
)
(
ind
:
Bool
)
:
MetaM
Unit
Equations
Instances For
source
def
Lean
.
mkBRecOn
(
declName
:
Name
)
:
MetaM
Unit
Equations
Instances For
source
def
Lean
.
mkBInductionOn
(
declName
:
Name
)
:
MetaM
Unit
Equations
Instances For