syntax objects for structure update expressions

Stream: lean4

[Simon Hudon]

I'm trying to construct a syntax object for a structure update. The following gives me an error:

def test (t x : Syntax) : TermElabM Syntax :=
`(λ a : $t => { a with $x := 0 })

error:

expected '}'

located on :=. If I replace $x with x, the error disappears. How can I get around that?

[Mario Carneiro]

def test (t x : Syntax) : TermElabM Syntax :=
`(λ a : $t => { a with $x:ident := 0 })

[Simon Hudon]

Thanks! Why is that necessary?

[Mario Carneiro]

Because the left hand side of a structure update can be more than just an identifier in lean 4. I'm not sure what is actually supported so far, but I believe it syntactically supports things like { s with foo.bar[1] := a }

[Mario Carneiro]

structure Foo :=
  bar : Array Nat
  y : Nat
structure Bar :=
  foo : Foo
  y : Nat

#check fun s : Bar => { s with foo.bar[1] := 1 }