source
def Lean.Elab.Structural.prettyParam (xs : Array Expr) (i : Nat) :
MetaM MessageData
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Structural.prettyRecArg (xs : Array Expr) (value : Expr) (recArgInfo : RecArgInfo) :
MetaM MessageData
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Structural.prettyParameterSet (fnNames : Array Name) (xs values : Array Expr) (recArgInfos : Array RecArgInfo) :
MetaM MessageData
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Structural.getRecArgInfo (fnName : Name) (fixedParamPerm : FixedParamPerm) (xs : Array Expr) (i : Nat) :
MetaM RecArgInfo

Assemble the `RecArgInfo` for the `i`th parameter in the parameter list `xs`. This performs various sanity checks on the parameter (is it even of inductive type etc).

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Structural.getRecArgInfos (fnName : Name) (fixedParamPerm : FixedParamPerm) (xs : Array Expr) (value : Expr) (termMeasure? : Option TerminationMeasure) :
MetaM (Array RecArgInfo × MessageData)

Collects the `RecArgInfos` for one function, and returns a report for why the others were not considered.

The `xs` are the fixed parameters, `value` the body with the fixed prefix instantiated.

Takes the optional user annotation into account (`termMeasure?`). If this is given and the measure is unsuitable, throw an error.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Structural.nonIndicesFirst (recArgInfos : Array RecArgInfo) :
Array RecArgInfo

Reorders the `RecArgInfos` of one function to put arguments that are indices of other arguments last. See issue #837 for an example where we can show termination using the index of an inductive family, but we don't get the desired definitional equalities.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Structural.inductiveGroups (recArgInfos : Array RecArgInfo) :
MetaM (Array IndGroupInst)

Given the `RecArgInfo`s of all the recursive functions, find the inductive groups to consider.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Structural.argsInGroup (group : IndGroupInst) (xs : Array Expr) (value : Expr) (recArgInfos : Array RecArgInfo) :
MetaM (Array RecArgInfo)

Filters the `recArgInfos` by those that describe an argument that's part of the recursive inductive group `group`.

Because of nested inductives this function has the ability to change the `recArgInfo`. Consider

    inductive Tree where | node : List Tree → Tree

then when we look for arguments whose type is part of the group `Tree`, we want to also consider the argument of type `List Tree`, even though that argument’s `RecArgInfo` refers to initially to `List`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Structural.maxCombinationSize :
Nat
Equations

- Lean.Elab.Structural.maxCombinationSize = 10

Instances For

source
def Lean.Elab.Structural.allCombinations {α : Type u_1} (xss : Array (Array α)) :
Option (Array (Array α))
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Structural.tryAllArgs {α : Type} (fnNames : Array Name) (fixedParamPerms : FixedParamPerms) (xs values : Array Expr) (termMeasure?s : Array (Option TerminationMeasure)) (k : Array RecArgInfo → M α) :
M α
Equations

- One or more equations did not get rendered due to their size.

Instances For