Open samuelgruetter opened 4 years ago
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.
?
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
?