Currently,
is parsed as
I think it would be more intuitive if it was parsed as
because I often pass updated records to a function, so I could write
and for updating the result of a function application, writing
seems fine to me, whereas
looks like superfluous parentheses.
Could we do something like
Notation "x <| proj := v |>" := (set proj (fun _ => v) x)
(at level 8, left associativity, format "x <| proj := v |>") : record_set.
?