Hi. I'm trying to use the coq-record-update library in my code and stumbled upon the following curiosity.
Require Import Program.
From RecordUpdate Require Import RecordSet.
Record X := mkX { a : list nat ; b : ~ In 0 a }.
#[local] Instance etaX : Settable _ :=
settable! mkX <a; b>.
Program Definition x1 := {| a := nil ; b := _ |}.
Definition x2 := set a (fun x => cons 1 x) x1.
From the code above I get the following error.
Error:
The following term contains unresolved implicit arguments:
(set a (fun x : list nat => 1 :: x) x1)
More precisely:
- ?Setter: Cannot infer the implicit parameter Setter of
set whose type is "Setter a" (no type class instance
found).
Why do we get this cryptic error? I suspect it may be related to the fact that b references a. Is that a known limitation of the library? Can it be made to work with these kind of records?
Hi. I'm trying to use the
coq-record-updatelibrary in my code and stumbled upon the following curiosity.From the code above I get the following error.
Why do we get this cryptic error? I suspect it may be related to the fact that
breferencesa. Is that a known limitation of the library? Can it be made to work with these kind of records?