The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Wed, 4 May 2011 10:40:04 -0400,
Jianzhou Zhao 
<jianzhou AT seas.upenn.edu>
 a écrit :

> Hi,
> 
> Does Coq have a record-update syntax like OCaml?
> 
> type r = {f1:int; f2:int}
> let a = {f1:=0;f2=0}
> let b =  {a with f1 = 0}
> 
> Thank

No it hasn't.

If you know on which type you will need it and there is not too much
combinations, you can always do:

Notation "{[ a 'with' 'f1' := O ]}" := ({|f1 := O; f2 := a.(f2)|}).
or
Notation "{[ a 'with' 'f1' := O ]}" :=
 (match a with {|f1:=_; f2:=f2_|} => {|f1 := O; f2 := f2_ |} end).
or
Definition updatef1 a O :=
 match a with {|f1:=_; f2:=f2_|} => {|f1 := O; f2 := f2_ |} end.
Notation "{[ a 'with' 'f1' := O ]}" :=
 (updatef1 a O).
...

But remember that in any way, even if there was some special syntax for
that, in gallina it would be translated as above.

A possible feature would be to autogenerate the "update_[field]"
functions, like what is done with "[inductive]_ind", but it should be
ok to change only one field (if you want to be exhaustive you have 2^n
cases and we do not wish to generate so many cases), note also that due
to dependencies, there should be some complications:

Record example: Type
{ a: nat;
  Ha: a < 10;
}.

then updating the "a" field implies updating the "Ha" field.