On vectors
Do the same exercise as this one , but considering vectors instead of
lists
Solution
Look at this file
See also
Consider the following definition, very similar to Standard Library's
definition:
(** Similar to Vector_Def library, with different names
*)
Section Vector_definitions.
Variable A : Type.
Inductive vector : nat -> Type :=
| vnil : vector 0
| vcons (h:A)(n:nat)(v: vector n) : vector (S n).
Define the functions that return respectively the head and the tail of
a non-empty vector, as direct
applications of the recursor vector_rect>
Solution
Look at this file