coq-record-update
coq-record-update copied to clipboard
precedence between application and record update?
Currently,
f s <|Pc := v|>
is parsed as
(f s) <|Pc := v|>
I think it would be more intuitive if it was parsed as
f (s <|Pc := v|>)
because I often pass updated records to a function, so I could write
f s<|Pc := v|>
and for updating the result of a function application, writing
(f s)<|Pc := v|>
seems fine to me, whereas
f (s<|Pc := v|>)
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.
?