Inductives don't always split parameters from indices with the colon

[ia0]

This is mostly nit, but just in case it is unintended. (Otherwise feel free to close.)

I would naively expect the reference to follow the convention that inductive declarations use the colon to separate (uniform) parameters from indices. One place where the source code, the semantics, and the reference differ (which I find surprising because I would expect the reference to either reflect the source code or its semantics) is for HEq.

The source code says (relying on inductive.autoPromoteIndices I guess):

inductive HEq : {α : Sort u} → α → {β : Sort u} → β → Prop where
  | refl (a : α) : HEq a a

The semantics (#print HEq) says (number of parameters is 2, not 0 like above and not 1 like below):

Lean 4: inductive HEq.{u} : {α : Sort u} → α → {β : Sort u} → β → Prop
number of parameters: 2
constructors:
HEq.refl : ∀ {α : Sort u} (a : α), a ≍ a

The reference shows: