在 Coq 中更新单个记录字段

Question

在 Coq 中更新单个记录字段

4

我有一个拥有许多字段的记录类型：

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

我想有一个函数，可以更新这条记录中的任意一个字段。在Haskell中，我会这样做：

update2019 record x = record {field2019 = x}

我该如何在Coq中执行这样的操作？

- radrow

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Anton Trunov · Accepted Answer

很不幸，Coq不支持记录更新。但幸运的是，有一个coq-record-update库，由@tchajed开发，可以极大地简化这一过程。下面是一个示例：

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 |>.

请查看该库的README.md文件以获取更详细的信息。