Data.Hex

Definitions

parseHex : Char -> Maybe (Fin 16)

Totality: total
Visibility: export

hexDigit : Fin 16 -> Char

Totality: total
Visibility: export

leftPad : Char -> Nat -> String -> String

Totality: total
Visibility: export

fromHexLittleEndian : String -> Maybe Integer

  Convert little-endian hex-string to Integer.
  Fails if the string doesn't represent a hexadecimal number.
  As for the latin letters in the hex-string, both lower- and upper- case letters represent valid hex characters.
  Examples of valid hex-strings:
  FFF ✔
  fEA ✔
  hello ✗
  1F62aA7 ✔

Totality: total
Visibility: export

fromHexBigEndian : String -> Maybe Integer

  Just like `fromHexLittleEndian` but for big-endian hex-strings.

Totality: total
Visibility: export