export structure field shorthand

Stream: lean4

[Horațiu Cheval]

Is there a way to export a structure field right away when defining the structure?
Something like

class Box (α : Type) where
  export box : α → α

as a shorthand for

class Box (α : Type) where
  box : α → α
export Box (box)

[Henrik Böving]

If there is I haven't seen it so far so most likely no, the compiler also uses the 2nd notation all over the place.

[Mac]

I suggest this feature a while back in Field Exports [RFC]. The consensus seemed to be that while it is convenient sugar, it is not worth the cycles to implement.