Nikola Katić (Aug 10 2022 at 22:26): Nikola Katić (Aug 10 2022 at 22:26):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.
Karl Palmskog (Aug 10 2022 at 22:30):see here, this library is also part of the Coq Platform: https://github.com/tchajed/coq-record-update
Karl Palmskog (Aug 10 2022 at 22:35):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
Nikola Katić (Aug 10 2022 at 22:44):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
Karl Palmskog (Aug 10 2022 at 22:59):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: Oct 13 2024 at 01:02 UTC