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