How to delaborate structure constructors?

Stream: lean4

[Tomas Skrivan]

When I delaborate application of structure constructor I get anonymous { ... } syntax with no type specification. Elaborating it back fails.

import Lean

open Lean Meta PrettyPrinter Elab Term

structure Vector3 where
  (x y z : Float)

run_elab
  withLocalDeclD `x (.const ``Float []) fun x => do
    let e ← mkAppM ``Vector3.mk #[x,x,x]
    let stx ← delab e
    let e' ← elabTerm stx none
    logInfo e
    logInfo e'
    logInfo m!"round trip: {← isDefEq e e'}"

prints

{ x := x, y := x, z := x }
?m.1924
round trip: false

How do I make sure that the delaborator spits out { x := x, y := x, z := x : Vector3}?

[Robin Arnez]

set_option pp.structureInstanceTypes true

[Tomas Skrivan]

Thanks, works as expected now!