Documentation
Lean
.
Elab
.
PreDefinition
.
Structural
.
BRecOn
Search
Google site search
return to top
source
Imports
Lean.Elab.RecAppSyntax
Lean.Util.HasConstCache
Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.Structural.Basic
Lean.Meta.Match.MatcherApp.Transform
Imported by
Lean
.
Elab
.
Structural
.
mkBRecOn
source
def
Lean
.
Elab
.
Structural
.
mkBRecOn
(recFnName :
Lake.Name
)
(recArgInfo :
Lean.Elab.Structural.RecArgInfo
)
(value :
Lean.Expr
)
:
Lean.Elab.Structural.M
Lean.Expr
Equations
One or more equations did not get rendered due to their size.
Instances For