This module contains the types
IndGroupInfo
, a variant ofInductiveVal
with information that applies to a whole group of mutual inductives andIndGroupInst
which extendsIndGroupInfo
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.
Equations
Equations
Instances For
Instances For
Instantiates the right .brecOn
for the given type former index,
including universe parameters and fixed prefix.
Equations
Equations
- igi.toMessageData = Lean.MessageData.ofExpr (Lean.mkAppN (Lean.Expr.const igi.all[0]! igi.levels) igi.params)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Instances For
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.