Structure Extension Naming

Stream: lean4

[Marcus Rossel]

IIRC, in Lean 3 it was possible to name the extended instance when declaring a structure extension:

structure first :=
  (one : nat)

structure second extends f : first :=
  (two : nat)

Is there a way to do this in Lean 4, too? Or is the auto-generated toFirst the only way of accessing the extended instance right now?