Skip to content

Add Countable instance for vec

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

Loading