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

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

Equations

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

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

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

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

def Lean.Elab.Structural.getRecArgInfos (fnName : Lean.Name) (xs : Array Lean.Expr) (value : Lean.Expr) (termArg? : Option Lean.Elab.TerminationArgument) : Lean.MetaM (Array Lean.Elab.Structural.RecArgInfo × Lean.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 annotations into account (termArg?). If this is given and the argument is unsuitable, throw an error.

Equations

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

def Lean.Elab.Structural.nonIndicesFirst (recArgInfos : Array Lean.Elab.Structural.RecArgInfo) : Array Lean.Elab.Structural.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 Lean.Elab.Structural.RecArgInfo) : Lean.MetaM (Array Lean.Elab.Structural.IndGroupInst)

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

def Lean.Elab.Structural.argsInGroup (group : Lean.Elab.Structural.IndGroupInst) (xs : Array Lean.Expr) (value : Lean.Expr) (recArgInfos : Array Lean.Elab.Structural.RecArgInfo) : Lean.MetaM (Array Lean.Elab.Structural.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

Equations

• Lean.Elab.Structural.maxCombinationSize = 10

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.

@[irreducible]

def Lean.Elab.Structural.allCombinations.go {α : Type u_1} (xss : Array (Array α)) (i : Nat) (acc : Array α) : Array (Array α)

Equations

• Lean.Elab.Structural.allCombinations.go xss i acc = if h : i < xss.size then Array.flatMap (fun (x : α) => Lean.Elab.Structural.allCombinations.go xss (i + 1) (acc.push x)) xss[i] else #[acc]

def Lean.Elab.Structural.tryAllArgs {α : Type} (fnNames : Array Lean.Name) (xs values : Array Lean.Expr) (termArg?s : Array (Option Lean.Elab.TerminationArgument)) (k : Array Lean.Elab.Structural.RecArgInfo → Lean.Elab.Structural.M α) : Lean.Elab.Structural.M α

Equations

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