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