Documentation
Lean
.
Elab
.
PreDefinition
.
Structural
.
Main
Search
Google site search
return to top
source
Imports
Init
Lean.Elab.PreDefinition.Structural.BRecOn
Lean.Elab.PreDefinition.Structural.Basic
Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.PreDefinition.Structural.FindRecArg
Lean.Elab.PreDefinition.Structural.IndPred
Lean.Elab.PreDefinition.Structural.Preprocess
Lean.Elab.PreDefinition.Structural.SmartUnfolding
Imported by
Lean
.
Elab
.
Structural
.
structuralRecursion
source
def
Lean
.
Elab
.
Structural
.
structuralRecursion
(preDefs :
Array
Lean.Elab.PreDefinition
)
:
Lean.Elab.TermElabM
Unit
Equations
One or more equations did not get rendered due to their size.
Instances For