Interaction with ListNotations

[vmurali]

RocordSetNotations doesn't interact well with ListNotations. If you uncomment any of the imports, the program fails with a parse error

Error: Syntax error: ';' or ']' expected after [constr:operconstr level 200] (in [constr:operconstr]).

Require Import RecordUpdate.RecordSet List.

(* Import ListNotations. *)
Import RecordSetNotations.
(* Import ListNotations. *)

Record foo := { a : bool ;
                b : bool }.

Global Instance etaX_RtlExprs : Settable _ :=
  settable!
          Build_foo <a; b>.

Definition bar := {| a := true ; b := true |}.

Definition baz := bar[a := false].

I like the [] notation, but I prefer good interaction with ListNotations over less verbosity in record update notations.

[tchajed]

I ran into the same issue and had to avoid the update notation.

My plan is to steal the std++ notation for map insertions: <[k := a]> is the function insert k a : map -> map, so a couple updates to the map m look like <[k2 := a2]><[k1 := a1]>m. As a bonus, <[k := a]> represents the insertion function itself. The only downside is that the updates are inside-out, but they should commute anyway.

[vmurali]

Prefix updates, <[k2 := a2]><[k1 := a1]>m? That looks ugly. Can you not replace your [] with <[ ]>, keeping everything else the same ?

[tchajed]

Fair enough; to avoid conflicting with the std++ notations in case I need both at the same time I settled on <| f := v |>.