GitLab

This addresses #33 (closed)

I did not include any of the map lemmas, since we have versions of them for fmap (notation <$>).

I find the following lemma pretty weird:

Lemma vec_to_list_take_drop {A n} (i : fin n) (v : vec A n) :
  vtake i v ++ vdrop i v = v.
Proof. by rewrite vec_to_list_take, vec_to_list_drop, take_drop. Qed.

It involves implicit coercions to list, and it uses the append on lists.

Unless @lepigre has a good reason for it, I rather not include it.