CODEWITHSUNDEEP
recordcoq
radrow
radrow

Reputation: 7169

Update single record field in Coq

I have a record type with a lot of fields:

Record r : Set :=
  R {
    field1 : nat;
    field2 : nat;
    field3 : nat;
...
    field2137 : nat;
  }

I would like to have a function that will update just one field in this record. In Haskell I would do it like this

update2019 record x = record {field2019 = x}

How can I perform such an action in Coq?

Upvotes: 4

Views: 562

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15414

Unfortunately, Coq lacks support for record update. Luckily for us, there is coq-record-update library by @tchajed that greatly simplifies this. Here is an example:

From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.

Record r : Set :=
  R {
    f1 : nat;
    f2 : nat;
    f3 : nat;
  }.
Instance eta_r : Settable _ := settable! R <f1; f2; f3>.

Definition update3 record x : r := record <| f3 := x |>.

Please see the library's README.md file for more detail.

Upvotes: 5

Related Questions