bend-osdev-u32
Releases (1)
-
0.1.0.0 indexed
Definitions (397)
LAWS.bend
- law dbl_zero
- law dbl_add
- law dbl_dbl
- law dbl_lt
- law dbl_le
- law half_double
- law half_double_one
- law word_zero_value
- law word_value_lt
- law word_value_eq
- law word_cmp_value
- law word_not_value
- law word_add_wrap
- law word_add_value
- law word_sub_wrap
- law word_sub_value
- law word_inc_value
- law word_shl_value
- law word_shr_value
- law u32_cmp_value
- law u32_lt_value
- law u32_le_value
- law u32_eq_value
- law u32_value_eq
- law u32_add_wrap
- law u32_add_value
- law u32_sub_wrap
- law u32_sub_value
- law u32_inc_value
- law u32_shl_value
- law u32_shln_value
- law u32_shr_value
- law u32_witthe bounds can hold, and the wrapping cases happen: 2^32 - 1 + 1 wraps to 0, below the first operand; 0 - 1 borrows
- law dbl_vec
- law nat_add_zero
- law nat_add_succ
- law nat_add_comm
- law nat_add_assoc
- law nat_add_left_comm
- law nat_add_cancel
- law nat_mul_zero
- law nat_mul_one
- law nat_one_mul
- law nat_mul_succ
- law nat_mul_comm
- law nat_mul_assoc
- law nat_mul_left_comm
- law nat_mul_add
- law nat_add_mul
- law nat_double
- law dbl_comm
- law dbl_mul_l
- law dbl_mul_r
- law nat_le_refl
- law nat_le_add
- law nat_lt_add
- law nat_le_witness
- law nat_lt_witness
- law nat_succ_add_absurd
- law nat_div_unique
- law nat_mod_unique
- law dbl_nowrap
- law nat_odd_half
- law nat_odd_le
- law low_high
- law low_lt
- law low_unique
- law high_unique
- law low_add_dbl
- law low_small
- law word_mul_wrap
- law word_mul_low
- law word_mul_value
- law u32_mul_wrap
- law u32_mul_low
- law u32_mul_value
- law u32_divmod
- law u32_mod_lt
- law u32_div_zero
- law u32_mod_zero
- law word_and_comm
- law word_or_comm
- law word_xor_comm
- law word_and_or
- law word_xor_and
- law word_or_split
- law word_mask_value
- law word_and_mask
- law word_not_sub
- law u32_and_comm
- law u32_or_comm
- law u32_xor_comm
- law u32_and_or
- law u32_xor_and
- law u32_or_split
- law u32_and_mask
- law u32_and_65535the 16-bit mask, written as Base reads it (65535 = U32Word.mask(32, 16))
- law u32_not_sub
- law u32_shrn_value
- law u32_shln_low