title: Supplying section arguments for examples
body: <p>Consider this section:</p>
  
  <pre><code>Section MyMap.
  
  Variables D R : Type.
  
  Fixpoint mymap (f : D -&gt; R) (l : list D) : list R :=
    match l with
    | nil =&gt; nil
    | d :: t =&gt; f d :: mymap f t
    end.
  
  End MyMap.
  </code></pre>
  
  <p>Here I've used <code>Variables</code> to declare my domain and range types.  As a sanity check on the definition of my function, I would like to include an <code>Example</code>:</p>
  
  <pre><code>Example example_map_S : mymap S [0; 1; 2] = [1; 2; 3].
  Proof.
    simpl; trivial.
  Qed.
  </code></pre>
  
  <p>However it seems I can't do so within my section.  Instead I get:</p>
  
  <pre><code>Error: The term "S" has type "nat -&gt; nat" while it is expected to have type "D -&gt; R".
  </code></pre>
  
  <p>That's not too surprising, so let's try it another way:</p>
  
  <pre><code>Example example_map_S : @mymap nat nat S [0; 1; 2] = [1; 2; 3].
  Proof.
    simpl; trivial.
  Qed.
  </code></pre>
  
  <p>Which produces:</p>
  
  <pre><code>Error: The term "nat" has type "Set" while it is expected to have type "D -&gt; R".
  </code></pre>
  
  <p>I suppose that's fair, section-ized <code>Variables</code> aren't the same thing as implicit arguments.  But it still leaves the question!</p>
  
  <p>How can I supply concrete <code>Variables</code> to a term before closing the section, in order to create useful <code>Examples</code>?</p>