fact: Fixpoint PbitsToInt32 (p: seq bool): Int32 := match p with | true :: p => lor one (lsl (PbitsToInt32 p) one) | false :: p => lsl (PbitsToInt32 p) one | [::] => zero end.
imports: Coq(ZArith.ZArith Extraction) mathcomp.ssreflect.ssreflect mathcomp(ssrbool eqtype ssrnat seq fintype ssrfun tuple) Bits(bits)