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

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

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

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

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

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.

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.

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

Given the RecArgInfos of all the recursive functions, find the inductive groups to consider.

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.

def Lean.Elab.Structural.maxCombinationSize : Nat

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

structure Lean.Elab.Structural.RecArgCandidate : Type

A candidate argument combination to try for structural recursion.

• group : IndGroupInst
• comb : Array RecArgInfo

structure Lean.Elab.Structural.RecArgCandidates : Type

Result of findRecArgCandidates: candidate combinations and a diagnostic report.

• candidates : Array RecArgCandidate
• report : MessageData

def Lean.Elab.Structural.findRecArgCandidates (fnNames : Array Name) (fixedParamPerms : FixedParamPerms) (xs values : Array Expr) (termMeasure?s : Array (Option TerminationMeasure)) : MetaM RecArgCandidates

Precompute all candidate argument combinations for structural recursion. This performs the analysis that may need function axioms in the environment (via isDefEq, inferType, etc.) but does not run the callback that attempts to eliminate mutual recursion.

def Lean.Elab.Structural.tryCandidates {α : Type} (fnNames : Array Name) (xs values : Array Expr) (candidates : RecArgCandidates) (k : Array RecArgInfo → MetaM α) : MetaM α

Try each candidate argument combination for structural recursion. Uses commitIfNoEx to backtrack on failure.