coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER Cedric <Cedric.Auger AT lri.fr>
- To: Jianzhou Zhao <jianzhou AT seas.upenn.edu>
- Cc: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] record update
- Date: Wed, 4 May 2011 18:49:41 +0200
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.
- [Coq-Club] record update, Jianzhou Zhao
- Re: [Coq-Club] record update, AUGER Cedric
Archive powered by MhonArc 2.6.16.