coq-record-update
coq-record-update copied to clipboard
tchajed
Library to create Coq record update functions
Hello, After some trials, it seems that `coq-record-update` does not support the `Set Primitive Projections.` flag. Here is an example were we did not get the expected result: ```coq From...
Hi. I'm trying to use the `coq-record-update` library in my code and stumbled upon the following curiosity. ```coq Require Import Program. From RecordUpdate Require Import RecordSet. Record X := mkX...
The example given in Reade.md doesn't work as I would expect it. The function `setAB'` does what I think it should, but `setAB` has the wrong type - the `a`...
A while back, @JasonGross pointed out that you can obtain an eta expansion of a record's constructor without relying on user-provided typeclass instances like ```coq (* all you need to...
This MR adds update syntax similar to the syntax offered for record creation when storing functions. Instead of writing ```coq x plus m n |> ``` you can now write...
Currently, in `RecordSetTests.DependentExample`, we can't typecheck ```coq Definition setA(x: X)(a: T x) := x . ``` because `set` only accepts non-dependent projections `(proj: R -> T)`. This PR makes `set`...
Note that field-setting is up to unification, and so we fully normalize the type of the record when generating the instance. This will be very slow for large record types....
(Note: so far I've only used coq-record-update in one example file in riscv-coq which has become obsolete in the meantime, so the issue I'm raising here is not blocking me...
This is nice. I'm wondering if you've thought about the connection to lenses. I cooked up a (very simple) library for lenses (https://github.com/gmalecha/coq-lens) that has been fairly convenient in my...
Currently, ``` f s ``` is parsed as ``` (f s) ``` I think it would be more intuitive if it was parsed as ``` f (s ) ``` because...