parser category for structure fields?

Stream: lean4

[Paro]

I'm trying to write a macro for something like { e with $field := x }, but Lean parser keeps reporting "expected '}'" after $field.

[Arthur Paulino]

I think your syntax is conflicting with another syntax that already exists

[Mario Carneiro]

you need to specify that $field is an ident

[Mario Carneiro]

`({ e with $field:ident := x })

[Arthur Paulino]

@Mario Carneiro is it because of a conflict and specifying $ident removes it?

[Mario Carneiro]

it is because you can put more than just idents in that position

[Mario Carneiro]

i.e. { e with a[1] := 2 }