Returning a record from a definition in Coq

Viewed 230

Suppose I've got a record that contains two nats.

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

I want to build a definition that given two nats returns a record containing those two nats.

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

Unfortunately, the official documentation only seems to cover the simpler cases when the return type is a bool or a nat. Is such a thing possible in coq? If yes, what is the best method to achieve it?

Thanks

1 Answers
Related