从 Coq 中的定义返回记录

Question

假设我有一个包含两个 nats 的 record。

Record toy := {
    num1 : nat;
    num2 : nat
}.

我想建立一个定义，给定两个 nats return 一个包含这两个 nats 的 record。

Definition args_to_toy_record (n1 : nat) (n2 : nat) : toy := 
 (* {num1 = n1;  num2 = n2} ?? *)

不幸的是，官方文档似乎只涵盖了 return 类型是 bool 或 nat 的更简单的情况。 coq 有这种事吗？如果是，实现它的最佳方法是什么？

谢谢

Answer 1

你几乎是对的。您只需要稍微不同的语法：

Record toy := {
    num1 : nat;
    num2 : nat
}.

Definition args_to_toy_record (n1 : nat) (n2 : nat) : toy :=
 {| num1 := n1;  num2 := n2 |}.

或者，您可以使用常规构造函数语法。 Coq 中的每个记录 toto 都被声明为具有单个构造函数 Build_toto 的归纳（有时，coinductive）类型，其参数恰好是记录的字段：

Definition args_to_toy_record (n1 : nat) (n2 : nat) : toy :=
  Build_toy n1 n2.

您也可以明确命名记录构造函数，如下所示：

Record toy := Toy {
    num1 : nat;
    num2 : nat
}.

Definition args_to_toy_record (n1 : nat) (n2 : nat) : toy :=
  Toy n1 n2.

Returning a record from a definition in Coq