从Coq中的定义返回记录

Question

假设我有一个record包含两个nats.

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

我想构建一个给定两个包含这两个nats返回的定义.recordnats

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

不幸的是,官方文档似乎只涵盖了返回类型为a bool或a 时更简单的情况nat.这样的事情可能coq吗？如果是,实现它的最佳方法是什么？

谢谢

Answer 1

你几乎是对的.你只需要稍微不同的语法:

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

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

或者,您可以使用常规构造函数语法.totoCoq中的每个记录都被声明为具有单个构造函数的归纳(有时是coinductive)类型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.