Lean.Elab.PreDefinition.Structural.IndGroupInfo

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.

source

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

Instances For

source

instance Lean.Elab.Structural.instBEqIndGroupInfo :

BEq IndGroupInfo

Equations

Lean.Elab.Structural.instBEqIndGroupInfo = { beq := Lean.Elab.Structural.beqIndGroupInfo✝ }

source

instance Lean.Elab.Structural.instInhabitedIndGroupInfo :

Inhabited IndGroupInfo

Equations

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

source

instance Lean.Elab.Structural.instReprIndGroupInfo :

Repr IndGroupInfo

Equations

Lean.Elab.Structural.instReprIndGroupInfo = { reprPrec := Lean.Elab.Structural.reprIndGroupInfo✝ }

source

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

IndGroupInfo

Equations

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

source

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

Nat

Equations

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

source

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.

source

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

Instances For

source

instance Lean.Elab.Structural.instInhabitedIndGroupInst :

Inhabited IndGroupInst

Equations

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

source

instance Lean.Elab.Structural.instReprIndGroupInst :

Repr IndGroupInst

Equations

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

source

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)

source

instance Lean.Elab.Structural.instToMessageDataIndGroupInst :

ToMessageData IndGroupInst

Equations

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

source

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

MetaM Bool

Equations

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

source

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.

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

source

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.