Expand description
This module defines interpretation for bit vectors as vectors of machine integers of various size and signedness.
Constants§
- SIMPLIFICATION_
LEMMA - An F* attribute that marks an item as being an interpretation lemma.
Type Aliases§
- i8x16
- i8 vectors of size 16
- i8x32
- i8 vectors of size 32
- i16x8
- i16 vectors of size 8
- i16x16
- i16 vectors of size 16
- i32x4
- i32 vectors of size 4
- i32x8
- i32 vectors of size 8
- i64x2
- i64 vectors of size 2
- i64x4
- i64 vectors of size 4
- i128x1
- i128 vectors of size 1
- i128x2
- i128 vectors of size 2
- u16x8
- u16 vectors of size 8
- u16x16
- u16 vectors of size 16
- u32x4
- u32 vectors of size 4
- u32x8
- u32 vectors of size 8
- u64x2
- u64 vectors of size 2
- u64x4
- u64 vectors of size 4