Documentation
Lean
.
Elab
.
PreDefinition
.
Structural
.
Main
Search
return to top
source
Imports
Lean.Elab.PreDefinition.Mutual
Lean.Elab.PreDefinition.TerminationMeasure
Lean.Meta.Tactic.TryThis
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
.
withCommonTelescope
Lean
.
Elab
.
Structural
.
withCommonTelescope
.
go
Lean
.
Elab
.
Structural
.
reporttermMeasure
Lean
.
Elab
.
Structural
.
structuralRecursion
source
def
Lean
.
Elab
.
Structural
.
withCommonTelescope
{
α
:
Type
}
(
preDefs
:
Array
PreDefinition
)
(
k
:
Array
Expr
→
Array
Expr
→
M
α
)
:
M
α
Equations
Instances For
source
partial def
Lean
.
Elab
.
Structural
.
withCommonTelescope
.
go
{
α
:
Type
}
(
k
:
Array
Expr
→
Array
Expr
→
M
α
)
(
fvars
vals
:
Array
Expr
)
:
M
α
source
def
Lean
.
Elab
.
Structural
.
reporttermMeasure
(
preDef
:
PreDefinition
)
(
recArgPos
:
Nat
)
:
MetaM
Unit
Equations
Instances For
source
def
Lean
.
Elab
.
Structural
.
structuralRecursion
(
preDefs
:
Array
PreDefinition
)
(
termMeasure?s
:
Array
(
Option
TerminationMeasure
)
)
:
TermElabM
Unit
Equations
Instances For