Expand description
This module provides a specification-friendly bit vector type.
Modules§
- int_
vec_ interp - This module defines interpretation for bit vectors as vectors of machine integers of various size and signedness.
Structs§
- BitVec
- A fixed-size bit vector type.
Constants§
- REWRITE_
RULE - An F* attribute that indiquates a rewritting lemma should be applied
Functions§
- bitvec_
postprocess_ norm - This function is useful only for verification in F*.
Used with
postprocess_rewrite, this tactic: