search

tchajed / coq-record-update

Library to create Coq record update functions
MIT License
42 stars 16 forks source link

Notation for nested record updates #7

Closed jakobbotsch closed 4 years ago

jakobbotsch commented 5 years ago

In my project I frequently need to update fields of nested records. The best way to do so seems to be something like

x<|f1 ::= set f2 (fun _ => v)|>

which is not particularly readable. Instead I have defined the notation

  Notation "x <| proj1 ; proj2 ; .. ; projn := v |>" :=
    (set proj1 (set proj2 .. (set projn (constructor v)) ..) x)
    (at level 12, left associativity).
  Notation "x <| proj1 ; proj2 ; .. ; projn ::= f |>" :=
    (set proj1 (set proj2 .. (set projn f) ..) x)
    (at level 12, left associativity).

allowing me to write

x<|f1; f2 := v|>
x<|f1; f2 ::= S|>

What do you think about adding this notation to the library? If it sounds good I can open a PR.

Also thanks for this great project, it has made using records in Coq much more enjoyable!

tchajed commented 4 years ago

Sounds good, we probably also have a few places that could use this notation!

Feel free to open a PR. The only thing I'll ask is that you use (fun _ => v) instead of constructor - that alias was only supposed to be for defining Settable and then I managed to hide even that from the user with settable!.