structure extend syntax

Stream: lean4

[James Gallicchio]

I noticed that the extends syntax on structures comes before the sort annotation for the structure, as here:

class LawfulSeq (C : Type u) (τ : outParam (Type v)) [Seq C τ]
  extends
    Mem.ToList C τ,
    Append.ToList C τ,
    Insert.ToMultiset C τ
  : Prop
  where

is this intended? It looks pretty unintuitive to me -- I was expecting Prop before extends, as

class LawfulSeq (C : Type u) (τ : outParam (Type v)) [Seq C τ]  : Prop
  extends
    Mem.ToList C τ,
    Append.ToList C τ,
    Insert.ToMultiset C τ
  where

[James Gallicchio]

Should I make an RFC about this? I know it's low priority, just don't want to forget about it