This is a Coq library for bit vectors. A bit vector is represented as bitseq (i.e. seq bool) with LSB at the head and MSB at the last.

Requirements

• Coq (>= 8.13.1)
• coq-mathcomp-ssreflect, coq-mathcomp-algebra (>= 1.12.0)

Build Status

• OCaml 4.12.1, Coq 8.13.2, mathcomp 1.12.0: OK
• OCaml 4.13.1, Coq 8.14.1, mathcomp 1.13.0: OK
• OCaml 4.14.0, Coq 8.15.2, mathcomp 1.14.0: OK
• OCaml 4.14.0, Coq 8.16.0, mathcomp 1.15.0: OK