coq-record-update icon indicating copy to clipboard operation
coq-record-update copied to clipboard

precedence between application and record update?

Open samuelgruetter opened this issue 4 years ago • 0 comments

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.

?

samuelgruetter avatar Oct 07 '20 16:10 samuelgruetter