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 Lean.Name
• numNested : Nat

instance Lean.Elab.Structural.instBEqIndGroupInfo : BEq Lean.Elab.Structural.IndGroupInfo

instance Lean.Elab.Structural.instInhabitedIndGroupInfo : Inhabited Lean.Elab.Structural.IndGroupInfo

instance Lean.Elab.Structural.instReprIndGroupInfo : Repr Lean.Elab.Structural.IndGroupInfo

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

Equations

• Lean.Elab.Structural.IndGroupInfo.ofInductiveVal indInfo = { all := indInfo.all.toArray, numNested := indInfo.numNested }

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

Equations

• group.numMotives = group.all.size + group.numNested

partial def Lean.Elab.Structural.IndGroupInfo.brecOnName (info : Lean.Elab.Structural.IndGroupInfo) (ind : Bool) (idx : Nat) : Lean.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 Lean.Name
• numNested : Nat
• levels : List Lean.Level
• params : Array Lean.Expr

instance Lean.Elab.Structural.instInhabitedIndGroupInst : Inhabited Lean.Elab.Structural.IndGroupInst

Equations

• Lean.Elab.Structural.instInhabitedIndGroupInst = { default := { toIndGroupInfo := default, levels := default, params := default } }

instance Lean.Elab.Structural.instReprIndGroupInst : Repr Lean.Elab.Structural.IndGroupInst

Equations

• Lean.Elab.Structural.instReprIndGroupInst = { reprPrec := Lean.Elab.Structural.reprIndGroupInst✝ }

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

Equations

• igi.toMessageData = Lean.MessageData.ofExpr (Lean.mkAppN (Lean.Expr.const igi.all[0]! igi.levels) igi.params)

instance Lean.Elab.Structural.instToMessageDataIndGroupInst : Lean.ToMessageData Lean.Elab.Structural.IndGroupInst

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

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

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

Equations

• group.brecOn ind lvl idx = Lean.mkAppN (Lean.Expr.const (group.brecOnName ind idx) (if ind = true then group.levels else lvl :: group.levels)) group.params

def Lean.Elab.Structural.IndGroupInst.nestedTypeFormers (igi : Lean.Elab.Structural.IndGroupInst) : Lean.MetaM (Array Lean.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]