Consider this section:
Section MyMap.
Variables D R : Type.
Fixpoint mymap (f : D -> R) (l : list D) : list R :=
match l with
| nil => nil
| d :: t => f d :: mymap f t
end.
End MyMap.
Here I've used Variables to declare my domain and range types. As a sanity check on the definition of my function, I would like to include an Example:
Example example_map_S : mymap S [0; 1; 2] = [1; 2; 3].
Proof.
simpl; trivial.
Qed.
However it seems I can't do so within my section. Instead I get:
Error: The term "S" has type "nat -> nat" while it is expected to have type "D -> R".
That's not too surprising, so let's try it another way:
Example example_map_S : @mymap nat nat S [0; 1; 2] = [1; 2; 3].
Proof.
simpl; trivial.
Qed.
Which produces:
Error: The term "nat" has type "Set" while it is expected to have type "D -> R".
I suppose that's fair, section-ized Variables aren't the same thing as implicit arguments. But it still leaves the question!
How can I supply concrete Variables to a term before closing the section, in order to create useful Examples?
Section MyMap.
...
If we check the type of mymap inside the section, we get
Check mymap.
(* mymap : (D -> R) -> list D -> list R *)
Of course, we can't unify D and R with nat, since D and R are some locally postulated types.
However, we can sort of simulate your example in this generalized setting, showing the expected property of the mymap function:
Example example_nil (f : D -> R) :
mymap f [] = [] := eq_refl.
Example example_3elems (f : D -> R) (d0 d1 d2 : D) :
mymap f [d0; d1; d2] = [f d0; f d1; f d2] := eq_refl.
End MyMap.