Changing a single field of a structure object

Stream: lean4

[Alex Keizer]

Currently I have a some functions that change one or two fields, like in

def DataView.pushLiveBinder (view : DataView) (binderIdent : Syntax) : DataView
  :=  let liveBinders := /* ... */
      let binders          := /* ... */
      {
        liveBinders, binders,

        ref             := view.ref
        declId          := view.declId
        modifiers       := view.modifiers
        shortDeclName   := view.shortDeclName
        declName        := view.declName
        levelNames      := view.levelNames
        type?           := view.type?
        ctors           := view.ctors
        derivingClasses := view.derivingClasses
        command         := view.command
        deadBinders     := view.deadBinders
        deadBinderNames := view.deadBinderNames
      }

Which really is just 80% noise. Is there a nicer syntax to say "now fill the rest of the fields with the values from this other object", without having to repeat each and every field?

[Mario Carneiro]

{ view with liveBinders, binders }

[Alex Keizer]

Ahh, I knew there was something, thanks!

[Trebor Huang]

By the way, this can be nested { myrec with a.b.c := d }, so it is super useful.