The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

Hello,

I don't know of any builtin ways to do this, but you can do it with a little bit of reflection. I can't seem to find my latest version, but something like the code that is located here will give you the ocaml-style with notation. Proving things about them is a little painful, but they compute nicely. I'll look for my other version which has better proof support if you're interested.

http://www.people.fas.harvard.edu/~gmalecha/proj/With.v

Hope this helps.

On Wed, Jul 28, 2010 at 7:44 AM, Jean-Marie Madiot <madiot AT gmail.com> wrote:

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

--
gregory malecha