Bit-vector specification

The overflow predicates produce Bool, while bvUltbv/bvSltbv produce a one-bit bit-vector.

Bitwise, arithmetic, shifts and comparison

Overflow predicates and conversions

Indexed operators

Constructors

The size is an index, so it is an explicit Nat and also fixes the result's own size.