title: Returning a record from a definition in Coq
body: <p>Suppose I've got a <code>record</code> that contains two <code>nats</code>. </p>
  
  <pre><code>Record toy := {
      num1 : nat;
      num2 : nat
  }.
  </code></pre>
  
  <p>I want to build a definition that given two <code>nats</code> returns a <code>record</code> containing those two <code>nats</code>. </p>
  
  <pre><code>Definition args_to_toy_record (n1 : nat) (n2 : nat) : toy := 
   (* {num1 = n1;  num2 = n2} ?? *)
  </code></pre>
  
  <p>Unfortunately, the official documentation only seems to cover the simpler cases when the return type is a <code>bool</code> or a <code>nat</code>. Is such a thing possible in <code>coq</code>? If yes, what is the best method to achieve it?</p>
  
  <p>Thanks</p>