coq - 从 Coq 的定义中返回一条记录

Question

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

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

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

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

不幸的是，官方文档似乎只涵盖了返回类型为 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 的归纳(有时是协合)类型，其参数正是记录的字段:

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.