coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Record with notation

From: Pierre Néron <pierre.neron AT polytechnique.org>
To: coq-club AT inria.fr
Subject: [Coq-Club] Record with notation
Date: Fri, 13 May 2016 11:54:18 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.neron AT gmail.com; spf=Pass smtp.mailfrom=pierre.neron AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f43.google.com
Ironport-phdr: 9a23:mGeYlB2gV/LqLuZ3smDT+DRfVm0co7zxezQtwd8ZsegSLPad9pjvdHbS+e9qxAeQG96LurQe0qGP7+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6DyZ7unLnus7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGDOO62EGX1IwEwBPBUCR9BD3RI389C33rO178DGdOdzqQLs0XzW78qotTwXn3nRUfwUl+X3a35QjxJlQpwis8kRy

Is there a way to define in Coq a notation similar to OCaml "with" notation for records ?

{ rec with foo := bar} would be a record with the same fields as "rec" except for field "foo" which would have value bar.

I did not manage to define one even for a specific record type.

Thanks in advance

--
Pierre Neron

[Coq-Club] Record with notation, Pierre Néron, 05/13/2016
- Re: [Coq-Club] Record with notation, Gregory Malecha, 05/13/2016
  - Re: [Coq-Club] Record with notation, Pierre Néron, 05/17/2016
    - Re: [Coq-Club] Record with notation, Gregory Malecha, 05/17/2016