从Coq定义中返回记录

Question

假设我有一个record，其中包含两个nats。

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

或者，您可以使用常规构造函数语法。在勒柯克每条记录toto被声明为感应（有时，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.