Refer to currently defined struct

Stream: lean4

[Horațiu Cheval]

Is there a syntax for referring to a field of the structure currently being defined when defining another field of it? I guess like some sort of an OOP this object.

structure Struct where
  a : Int
  b : Int

def mkStruct : Struct :=
  {
    a := 5
    b := a + 1  -- meaning the `a` of this structure instead of some other `a`
  }

which would be a shorthand for something like

def mkStruct : Struct :=
  let this.a := 5
  {
    a := this.a
    b := this.a + 1
  }

[Sky Wilshaw]

There's refine_struct in lean 3 but not in lean 4 yet.

[Sky Wilshaw]

I think that this has some related tactics that allow you to refer to previously defined fields.