Skip to content

Add Countable instance for vec

Tej Chajed requested to merge tchajed/stdpp:vec-countable into master

I was surprised to learn this wasn't available and managed to prove it.

Note that this pulls in stdpp.vector into countable. The only reason for this is that the proof is really simple with vec_to_list as defined in std++, as opposed to with Coq's Vector.of_list. This only affects users in that countable now loads vector, which for example changes the implicits on Coq's vectors.

Merge request reports