Coqの定義からレコードを返す

Question

に2つのnatsが含まれているとします。

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

私は2つのnatsはこれら2 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は、その引数がレコードの正確フィールドです単一コンストラクタBuild_toto、と入力します（時々、coinductive）誘導性として宣言されています。

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.