Question about `InductiveVal`

Stream: lean4

[Arthur Paulino]

In Lean/Declaration.lean we have:

structure InductiveVal extends ConstantVal where
  ...
  /-- List of all (including this one) inductive datatypes in the mutual declaration containing this one -/
  all : List Name
  ...

My question is: will that list be in the same order for every inductive from the same mutual block?

[Arthur Paulino]

Another question: if so, which order is it? Is it the order of appearance? Alphabetical order?

[Leonardo de Moura]

My question is: will that list be in the same order for every inductive from the same mutual block?

Yes

Another question: if so, which order is it? Is it the order of appearance? Alphabetical order?

The all field is set by the kernel, and it uses the order used in the field types : List InductiveType at the Declaration.inductDecl constructor.
The current inductive command uses the declaration order for setting this field.