Retour d'un enregistrement à partir d'une définition dans Coq

Question

Supposons que j'ai un record qui contient deux nats.

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

Je veux construire une définition qui donne deux nats renvoie un record contenant ces deux nats.

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

Malheureusement, la documentation officielle semble que pour couvrir les cas les plus simples lorsque le type de retour est un bool ou un nat. Est-ce une telle chose possible dans coq? Si oui, quelle est la meilleure méthode pour y parvenir?

Merci

Answer 1

Vous l'avez eu presque raison. Vous avez juste besoin d'une syntaxe légèrement différente:

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

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

Vous pouvez également utiliser la syntaxe de constructeur standard. Chaque enregistrement toto en Coq est déclaré comme un inducteur (parfois, CoInductive) type avec un seul constructeur Build_toto, dont les arguments sont exactement les champs de l'enregistrement:

Definition args_to_toy_record (n1 : nat) (n2 : nat) : toy := 
    Build_toy n1 n2. 

Vous pouvez également nommer le constructeur d'enregistrement explicitement, comme celui-ci :

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

Definition args_to_toy_record (n1 : nat) (n2 : nat) : toy := 
    Toy n1 n2.