The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello, Pierre --

I hacked something like this together a while ago. The latest incarnation is probably not quite up to snuff but the ideas can be found in this file:

https://github.com/coq-ext-lib/coq-ext-lib/blob/v8.5/theories/Programming/With.v

Note: To use this code you need to declare some type class instances (namely Struct and Accessor) for records that you would like to do this for.

I'd be happy to chat more with you about it and fix up the code to make it easier to use. One thing that I think is important about this implementation is that 'with' desugars definitionally/judgementally rather than just propositionally which is very important for computation.

On Fri, May 13, 2016 at 2:54 AM, Pierre Néron <pierre.neron AT polytechnique.org> wrote:

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

--

gregory malecha

gmalecha.github.io