The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Glad to hear that it works. While there is a lot of boiler-plate, I don't think that it is too complex. The way that Haskell solves the complexity issue (e.g. with Lens's) is to generate definitions automatically. Something like that is probably what we want to do to make it easier to use.

On Tue, May 17, 2016 at 4:11 AM, Pierre Néron <pierre.neron AT polytechnique.org> wrote:

Thanks, it worked out of the box. Something simpler would indeed be nice but at least it does the job.

Pierre Neron

On 05/13/2016 06:57 PM, Gregory Malecha wrote:

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

--

gregory malecha

gmalecha.github.io