package coq-stdpp-bitvector

This library provides the bv n type for representing n-bit bitvectors (i.e., fixed-size integers with n bits). It comes with definitions for the standard operations (e.g., the operations exposed by SMT-LIB) and some basic automation for solving bitvector goals based on the lia tactic.