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

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:

Start by comparing the reference-manual rendering of HEq with the source declaration in Init/Prelude.lean and the output of #print HEq, focusing on how the colon separates parameters from indices. Done means the reference consistently reflects the intended parameter count and declaration structure.