This module contains the types

• IndGroupInfo, a variant of InductiveVal with information that applies to a whole group of mutual inductives and
• IndGroupInst which extends IndGroupInfo with levels and parameters to indicate a instantiation of the group.

One purpose of this abstraction is to make it clear when a function operates on a group as a whole, rather than a specific inductive within the group.

structure Lean.Elab.Structural.IndGroupInfo : Type

A mutually inductive group, identified by the all array of the InductiveVal of its constituents.

• all : Array Name
• numNested : Nat

instance Lean.Elab.Structural.instBEqIndGroupInfo : BEq IndGroupInfo

instance Lean.Elab.Structural.instInhabitedIndGroupInfo : Inhabited IndGroupInfo

instance Lean.Elab.Structural.instReprIndGroupInfo : Repr IndGroupInfo

def Lean.Elab.Structural.IndGroupInfo.ofInductiveVal (indInfo : InductiveVal) : IndGroupInfo

def Lean.Elab.Structural.IndGroupInfo.numMotives (group : IndGroupInfo) : Nat

partial def Lean.Elab.Structural.IndGroupInfo.brecOnName (info : IndGroupInfo) (ind : Bool) (idx : Nat) : Name

Instantiates the right .brecOn or .bInductionOn for the given type former index, including universe parameters and fixed prefix.

structure Lean.Elab.Structural.IndGroupInstextends Lean.Elab.Structural.IndGroupInfo : Type

An instance of an mutually inductive group of inductives, identified by the all array and the level and expressions parameters.

For example this distinguishes between List α and List β so that we will not even attempt mutual structural recursion on such incompatible types.

• all : Array Name
• numNested : Nat
• levels : List Level
• params : Array Expr

instance Lean.Elab.Structural.instInhabitedIndGroupInst : Inhabited IndGroupInst

instance Lean.Elab.Structural.instReprIndGroupInst : Repr IndGroupInst

def Lean.Elab.Structural.IndGroupInst.toMessageData (igi : IndGroupInst) : MessageData

instance Lean.Elab.Structural.instToMessageDataIndGroupInst : ToMessageData IndGroupInst

def Lean.Elab.Structural.IndGroupInst.isDefEq (igi1 igi2 : IndGroupInst) : MetaM Bool

def Lean.Elab.Structural.IndGroupInst.brecOn (group : IndGroupInst) (ind : Bool) (lvl : Level) (idx : Nat) : Expr

Instantiates the right .brecOn or .bInductionOn for the given type former index, including universe parameters and fixed prefix.

def Lean.Elab.Structural.IndGroupInst.nestedTypeFormers (igi : IndGroupInst) : MetaM (Array Expr)

Figures out the nested type formers of an inductive group, with parameters instantiated and indices still forall-abstracted.

For example given a nested inductive

inductive Tree α where | node : α → Vector (Tree α) n → Tree α

(where n is an index of Vector) and the instantiation Tree Int it will return

#[(n : Nat) → Vector (Tree Int) n]