Name structure constructor

Stream: lean4

[Marcus Rossel]

Is there a way to given a structure's constructor a different name than mk? (Aside from declaring it with inductive and losing all the structure niceties)

[Kyle Miller]

Yes https://leanprover.github.io/lean4/doc/struct.html https://leanprover.github.io/lean4/doc/declarations.html#structures-and-records

structure Point (α : Type u) where
  create ::
  x : α
  y : α

[Chris B]

structure A := myCtor ::
(field1 : Nat)
(field2 : Char)

[Chris B]

Beat me to it.