The Coq mailing list

[Jean-Marie Madiot <madiot AT gmail.com>]

Hello all,

I'm currently using the Record syntactic sugar and I was wondering if
it is possible to build a record instance from an existing one while
modifying only a few fields. To be clear, I have a record with many
fields, like this:

 Record rec := rec_cons {
   rec1 : nat;
   rec2 : nat;
   rec3 : nat;
   recdots : nat
 }.

(* and I built an instance of rec: *)

 Definition r : rec := rec_cons 1 2 3 4.
 Definition r2 : rec := {| rec1 := 1; rec2 := 2; rec3 := 3; recdots
:= 4 |}. (* same thing *)

(* now I want to make an instance based on r but modifying only one
field, like that: *)

 Definition r' : rec := {| r with rec2 := 20 |}.

But it does not work like that. (This is inspired from the ocaml
syntax). Is there another way? I know I can do such a thing by
defining my own function depending on my record type and which field I
want to alter -- and even setting up a notation for it -- but since
records are already just syntactic sugar, maybe it is possible to have
something more general?

Or maybe it interferes with the existing notation system?

Regards,

Jean-Marie