在Coq中从定义中返回一条记录

Question

假设我有一个包含两个自然数的记录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中是否可能实现这种功能？如果是，最佳方法是什么？

谢谢。

- iamwhoiam

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.

- Arthur Azevedo De Amorim