package libsail

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Libsail.Sail2_operators_bitlistsSource

Sourceval uint_maybe : Sail2_values.bitU list -> Nat_big_num.num option
Sourceval uint : Sail2_values.bitU list -> Nat_big_num.num
Sourceval sint_maybe : Sail2_values.bitU list -> Nat_big_num.num option
Sourceval sint : Sail2_values.bitU list -> Nat_big_num.num
Sourceval extz_vec : Nat_big_num.num -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval exts_vec : Nat_big_num.num -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval zero_extend : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval sign_extend : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval zeros : Nat_big_num.num -> Sail2_values.bitU list
Sourceval ones : Nat_big_num.num -> Sail2_values.bitU list
Sourceval vector_truncate : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval vector_truncateLSB : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval access_vec_inc : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU
Sourceval access_vec_dec : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU
Sourceval update_vec_inc : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU -> Sail2_values.bitU list
Sourceval update_vec_inc_maybe : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU -> Sail2_values.bitU list option
Sourceval update_vec_dec : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU -> Sail2_values.bitU list
Sourceval update_vec_dec_maybe : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU -> Sail2_values.bitU list option
Sourceval subrange_vec_inc : Sail2_values.bitU list -> Nat_big_num.num -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval subrange_vec_dec : Sail2_values.bitU list -> Nat_big_num.num -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval update_subrange_vec_inc : Sail2_values.bitU list -> Nat_big_num.num -> Nat_big_num.num -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval update_subrange_vec_dec : Sail2_values.bitU list -> Nat_big_num.num -> Nat_big_num.num -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval concat_vec : Sail2_values.bitU list -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval cons_vec_maybe : Sail2_values.bitU -> Sail2_values.bitU list -> Sail2_values.bitU list option
Sourceval cast_unit_vec : Sail2_values.bitU -> Sail2_values.bitU list
Sourceval cast_unit_vec_maybe : Sail2_values.bitU -> Sail2_values.bitU list option
Sourceval vec_of_bit : Nat_big_num.num -> Sail2_values.bitU -> Sail2_values.bitU list
Sourceval vec_of_bit_maybe : Nat_big_num.num -> Sail2_values.bitU -> Sail2_values.bitU list option
Sourceval int_of_vec_maybe : bool -> Sail2_values.bitU list -> Nat_big_num.num option
Sourceval int_of_vec : bool -> Sail2_values.bitU list -> Nat_big_num.num
Sourceval string_of_bits : Sail2_values.bitU list -> string
Sourceval string_of_bits_subrange : Sail2_values.bitU list -> Nat_big_num.num -> Nat_big_num.num -> string
Sourceval decimal_string_of_bits : Sail2_values.bitU list -> string
Sourceval not_vec : Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval arith_op_double_bl : 'a Sail2_values.bitvector_class -> (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) -> bool -> 'a -> 'a -> Sail2_values.bitU list
Sourceval adds_vec : Sail2_values.bitU list -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval subs_vec : Sail2_values.bitU list -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval mult_vec : Sail2_values.bitU list -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval mults_vec : Sail2_values.bitU list -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval add_vec_int : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval sub_vec_int : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval mult_vec_int : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval add_int_vec : Nat_big_num.num -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval sub_int_vec : Nat_big_num.num -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval mult_int_vec : Nat_big_num.num -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval add_vec_bool : 'a Sail2_values.bitvector_class -> 'a -> bool -> 'a
Sourceval add_vec_bit_maybe : 'a Sail2_values.bitvector_class -> 'a -> Sail2_values.bitU -> 'a option
Sourceval adds_vec_bool : 'a Sail2_values.bitvector_class -> 'a -> bool -> 'a
Sourceval adds_vec_bit_maybe : 'a Sail2_values.bitvector_class -> 'a -> Sail2_values.bitU -> 'a option
Sourceval sub_vec_bool : 'a Sail2_values.bitvector_class -> 'a -> bool -> 'a
Sourceval sub_vec_bit_maybe : 'a Sail2_values.bitvector_class -> 'a -> Sail2_values.bitU -> 'a option
Sourceval subs_vec_bool : 'a Sail2_values.bitvector_class -> 'a -> bool -> 'a
Sourceval subs_vec_bit_maybe : 'a Sail2_values.bitvector_class -> 'a -> Sail2_values.bitU -> 'a option
Sourceval shiftl : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval shiftr : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval arith_shiftr : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval rotl : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval rotr : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval mod_vec_maybe : Sail2_values.bitU list -> Sail2_values.bitU list -> Sail2_values.bitU list option
Sourceval quot_vec : Sail2_values.bitU list -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval quot_vec_maybe : Sail2_values.bitU list -> Sail2_values.bitU list -> Sail2_values.bitU list option
Sourceval quots_vec : Sail2_values.bitU list -> Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval quots_vec_maybe : Sail2_values.bitU list -> Sail2_values.bitU list -> Sail2_values.bitU list option
Sourceval mod_vec_int : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval mod_vec_int_maybe : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list option
Sourceval quot_vec_int : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval quot_vec_int_maybe : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list option
Sourceval replicate_bits : Sail2_values.bitU list -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval duplicate : Sail2_values.bitU -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval duplicate_maybe : Sail2_values.bitU -> Nat_big_num.num -> Sail2_values.bitU list option
Sourceval reverse_endianness : Sail2_values.bitU list -> Sail2_values.bitU list
Sourceval get_slice_int : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval set_slice_int : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Sail2_values.bitU list -> Nat_big_num.num
Sourceval slice : Sail2_values.bitU list -> Nat_big_num.num -> Nat_big_num.num -> Sail2_values.bitU list
Sourceval eq_vec : Sail2_values.bitU list -> Sail2_values.bitU list -> bool
Sourceval neq_vec : Sail2_values.bitU list -> Sail2_values.bitU list -> bool