Stream: Coq users

Topic: Record update


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Jan 29 2023 at 03:28 UTC