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

Equations

• Lean.Elab.Structural.instBEqIndGroupInfo = { beq := Lean.Elab.Structural.instBEqIndGroupInfo.beq }

def Lean.Elab.Structural.instBEqIndGroupInfo.beq : IndGroupInfo → IndGroupInfo → Bool

Equations

• Lean.Elab.Structural.instBEqIndGroupInfo.beq { all := a, numNested := a_1 } { all := b, numNested := b_1 } = (a == b && a_1 == b_1)
• Lean.Elab.Structural.instBEqIndGroupInfo.beq x✝¹ x✝ = false

def Lean.Elab.Structural.instInhabitedIndGroupInfo.default : IndGroupInfo

Equations

• Lean.Elab.Structural.instInhabitedIndGroupInfo.default = { all := default, numNested := default }

instance Lean.Elab.Structural.instInhabitedIndGroupInfo : Inhabited IndGroupInfo

Equations

• Lean.Elab.Structural.instInhabitedIndGroupInfo = { default := Lean.Elab.Structural.instInhabitedIndGroupInfo.default }

instance Lean.Elab.Structural.instReprIndGroupInfo : Repr IndGroupInfo

Equations

• Lean.Elab.Structural.instReprIndGroupInfo = { reprPrec := Lean.Elab.Structural.instReprIndGroupInfo.repr }

def Lean.Elab.Structural.instReprIndGroupInfo.repr : IndGroupInfo → Nat → Format

Equations

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

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

Equations

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

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

Equations

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

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

Instantiates the right .brecOn 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

Equations

• Lean.Elab.Structural.instInhabitedIndGroupInst = { default := Lean.Elab.Structural.instInhabitedIndGroupInst.default }

def Lean.Elab.Structural.instInhabitedIndGroupInst.default : IndGroupInst

Equations

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

def Lean.Elab.Structural.instReprIndGroupInst.repr : IndGroupInst → Nat → Format

Equations

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

instance Lean.Elab.Structural.instReprIndGroupInst : Repr IndGroupInst

Equations

• Lean.Elab.Structural.instReprIndGroupInst = { reprPrec := Lean.Elab.Structural.instReprIndGroupInst.repr }

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

Equations

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

instance Lean.Elab.Structural.instToMessageDataIndGroupInst : ToMessageData IndGroupInst

Equations

• Lean.Elab.Structural.instToMessageDataIndGroupInst = { toMessageData := Lean.Elab.Structural.IndGroupInst.toMessageData }

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

Equations

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

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

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

Equations

• group.brecOn lvl idx = Lean.mkAppN (Lean.Expr.const (group.brecOnName idx) (lvl :: group.levels)) group.params

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]

Equations

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