Utils.Bytes

Definitions

to_le : {auto {conArg:2909} : (FiniteBits a, Cast a Bits8)} -> {auto 0 _ : NonZero n} -> {auto 0 _ : n * 8 = bitSize} -> a -> Vect n Bits8

Visibility: export

to_be : {auto {conArg:3021} : (FiniteBits a, Cast a Bits8)} -> {auto 0 _ : NonZero n} -> {auto 0 _ : n * 8 = bitSize} -> a -> Vect n Bits8

Visibility: export

from_le : {auto {conArg:3069} : (FiniteBits a, Cast Bits8 a)} -> {auto 0 _ : NonZero n} -> {auto 0 _ : n * 8 = bitSize} -> Vect n Bits8 -> a

Visibility: export

from_be : {auto {conArg:3196} : (FiniteBits a, Cast Bits8 a)} -> {auto 0 _ : NonZero n} -> {auto 0 _ : n * 8 = bitSize} -> Vect n Bits8 -> a

Visibility: export

set_bit_to : {auto {conArg:3243} : Bits a} -> Bool -> Index -> a -> a

Visibility: export

to_bools_be' : {auto {conArg:3275} : FiniteBits a} -> (n : Fin (S bitSize)) -> a -> Vect (finToNat n) Bool

Visibility: export

to_bools_be : {auto {conArg:3328} : FiniteBits a} -> a -> Vect bitSize Bool

Visibility: export

le_to_integer : Foldable t => t Bits8 -> Integer

Visibility: export

be_to_integer : Foldable t => t Bits8 -> Integer

Visibility: export

integer_to_le : (n : Nat) -> Integer -> Vect n Bits8

Visibility: export

integer_to_be : (n : Nat) -> Integer -> Vect n Bits8

Visibility: export

to_digit : Bool -> Char

Visibility: export

show_bin : FiniteBits a => a -> String

Visibility: export

hex_lower : Bits8 -> Char

  if 0-15, then return the corresponding hex char
  otherwise returns a '?'

Visibility: export

show_hex : Bits8 -> String

Visibility: export

xxd : Foldable t => t Bits8 -> String

  takes a list of bytes and show them using `show_hex` interspersed by a whitespace

Visibility: export

string_to_ascii : String -> List Bits8

Visibility: export

ascii_to_string : List Bits8 -> String

Visibility: export

shiftL' : FiniteBits a => a -> Nat -> a

Visibility: export

shiftR' : FiniteBits a => a -> Nat -> a

Visibility: export

rotl : {auto {conArg:3871} : FiniteBits a} -> S n = bitSize => Fin (S n) -> a -> a

Visibility: export

rotr : {auto {conArg:3938} : FiniteBits a} -> S n = bitSize => Fin (S n) -> a -> a

Visibility: export