What is a standard way to update records?
E.g. in a case when record has a list field and only removal of the first element (if there is at least 2 elements) of that list should be performed.
I found this SO post, but I'm hoping there is a more convenient way.
see here, this library is also part of the Coq Platform: https://github.com/tchajed/coq-record-update
the library is to my knowledge the state of the art in record updating, as in, there is no built-in support in Coq itself or "better" libraries
It may be that I'm missing the point of having records, but what could be their advantage over something like this:
Inductive myrec : Type := MyRec (n : nat) (input : list ascii).
...if a task is that simple as just popping an element of
input list from time to time
if you use coq-record-update, you get (1) projection functions and (2) update notations. If you don't need either of those,
Inductive is essentially the same as
Record under the hood (after elaboration)
Last updated: Sep 23 2023 at 15:01 UTC