Idris2Doc : Data.Byte

Data.Byte

(source)
Definitions
byte_0 : Bits8
  ASCII code of '0'

  Totality: total
  Visibility: public export
byte_1 : Bits8
  ASCII code of '1'

  Totality: total
  Visibility: public export
byte_2 : Bits8
  ASCII code of '2'

  Totality: total
  Visibility: public export
byte_3 : Bits8
  ASCII code of '3'

  Totality: total
  Visibility: public export
byte_4 : Bits8
  ASCII code of '4'

  Totality: total
  Visibility: public export
byte_5 : Bits8
  ASCII code of '5'

  Totality: total
  Visibility: public export
byte_6 : Bits8
  ASCII code of '6'

  Totality: total
  Visibility: public export
byte_7 : Bits8
  ASCII code of '7'

  Totality: total
  Visibility: public export
byte_8 : Bits8
  ASCII code of '8'

  Totality: total
  Visibility: public export
byte_9 : Bits8
  ASCII code of '9'

  Totality: total
  Visibility: public export
byte_a : Bits8
  ASCII code of 'a'

  Totality: total
  Visibility: public export
byte_b : Bits8
  ASCII code of 'b'

  Totality: total
  Visibility: public export
byte_c : Bits8
  ASCII code of 'c'

  Totality: total
  Visibility: public export
byte_d : Bits8
  ASCII code of 'd'

  Totality: total
  Visibility: public export
byte_e : Bits8
  ASCII code of 'e'

  Totality: total
  Visibility: public export
byte_f : Bits8
  ASCII code of 'f'

  Totality: total
  Visibility: public export
byte_g : Bits8
  ASCII code of 'g'

  Totality: total
  Visibility: public export
byte_h : Bits8
  ASCII code of 'h'

  Totality: total
  Visibility: public export
byte_i : Bits8
  ASCII code of 'i'

  Totality: total
  Visibility: public export
byte_j : Bits8
  ASCII code of 'j'

  Totality: total
  Visibility: public export
byte_k : Bits8
  ASCII code of 'k'

  Totality: total
  Visibility: public export
byte_l : Bits8
  ASCII code of 'l'

  Totality: total
  Visibility: public export
byte_m : Bits8
  ASCII code of 'm'

  Totality: total
  Visibility: public export
byte_n : Bits8
  ASCII code of 'n'

  Totality: total
  Visibility: public export
byte_o : Bits8
  ASCII code of 'o'

  Totality: total
  Visibility: public export
byte_p : Bits8
  ASCII code of 'p'

  Totality: total
  Visibility: public export
byte_q : Bits8
  ASCII code of 'q'

  Totality: total
  Visibility: public export
byte_r : Bits8
  ASCII code of 'r'

  Totality: total
  Visibility: public export
byte_s : Bits8
  ASCII code of 's'

  Totality: total
  Visibility: public export
byte_t : Bits8
  ASCII code of 't'

  Totality: total
  Visibility: public export
byte_u : Bits8
  ASCII code of 'u'

  Totality: total
  Visibility: public export
byte_v : Bits8
  ASCII code of 'v'

  Totality: total
  Visibility: public export
byte_w : Bits8
  ASCII code of 'w'

  Totality: total
  Visibility: public export
byte_x : Bits8
  ASCII code of 'x'

  Totality: total
  Visibility: public export
byte_y : Bits8
  ASCII code of 'y'

  Totality: total
  Visibility: public export
byte_z : Bits8
  ASCII code of 'z'

  Totality: total
  Visibility: public export
byte_A : Bits8
  ASCII code of 'A'

  Totality: total
  Visibility: public export
byte_B : Bits8
  ASCII code of 'B'

  Totality: total
  Visibility: public export
byte_C : Bits8
  ASCII code of 'C'

  Totality: total
  Visibility: public export
byte_D : Bits8
  ASCII code of 'D'

  Totality: total
  Visibility: public export
byte_E : Bits8
  ASCII code of 'E'

  Totality: total
  Visibility: public export
byte_F : Bits8
  ASCII code of 'F'

  Totality: total
  Visibility: public export
byte_G : Bits8
  ASCII code of 'G'

  Totality: total
  Visibility: public export
byte_H : Bits8
  ASCII code of 'H'

  Totality: total
  Visibility: public export
byte_I : Bits8
  ASCII code of 'I'

  Totality: total
  Visibility: public export
byte_J : Bits8
  ASCII code of 'J'

  Totality: total
  Visibility: public export
byte_K : Bits8
  ASCII code of 'K'

  Totality: total
  Visibility: public export
byte_L : Bits8
  ASCII code of 'L'

  Totality: total
  Visibility: public export
byte_M : Bits8
  ASCII code of 'M'

  Totality: total
  Visibility: public export
byte_N : Bits8
  ASCII code of 'N'

  Totality: total
  Visibility: public export
byte_O : Bits8
  ASCII code of 'O'

  Totality: total
  Visibility: public export
byte_P : Bits8
  ASCII code of 'P'

  Totality: total
  Visibility: public export
byte_Q : Bits8
  ASCII code of 'Q'

  Totality: total
  Visibility: public export
byte_R : Bits8
  ASCII code of 'R'

  Totality: total
  Visibility: public export
byte_S : Bits8
  ASCII code of 'S'

  Totality: total
  Visibility: public export
byte_T : Bits8
  ASCII code of 'T'

  Totality: total
  Visibility: public export
byte_U : Bits8
  ASCII code of 'U'

  Totality: total
  Visibility: public export
byte_V : Bits8
  ASCII code of 'V'

  Totality: total
  Visibility: public export
byte_W : Bits8
  ASCII code of 'W'

  Totality: total
  Visibility: public export
byte_X : Bits8
  ASCII code of 'X'

  Totality: total
  Visibility: public export
byte_Y : Bits8
  ASCII code of 'Y'

  Totality: total
  Visibility: public export
byte_Z : Bits8
  ASCII code of 'Z'

  Totality: total
  Visibility: public export
inRange : (lo : Bits8) -> (hi : Bits8) -> Bits8 -> {auto 0 _ : lo <= hi = True} -> Bool
  Totality: total
  Visibility: public export
isDigit : Bits8 -> Bool
  Totality: total
  Visibility: public export
isLower : Bits8 -> Bool
  Totality: total
  Visibility: public export
isUpper : Bits8 -> Bool
  Totality: total
  Visibility: public export
isAlpha : Bits8 -> Bool
  Totality: total
  Visibility: public export
isAlphaNum : Bits8 -> Bool
  Totality: total
  Visibility: public export
isSpace : Bits8 -> Bool
  Returns true if the byte represents an ASCII whitespace character.

  Totality: total
  Visibility: public export
isNL : Bits8 -> Bool
  Returns true if the character represents a new line.

  Totality: total
  Visibility: public export
toUpper : Bits8 -> Bits8
  Convert a letter to the corresponding upper-case letter, if any.
  Non-letters are ignored.

  Totality: total
  Visibility: public export
toLower : Bits8 -> Bits8
  Convert a letter to the corresponding lower-case letter, if any.
  Non-letters are ignored.

  Totality: total
  Visibility: public export
isHexDigit : Bits8 -> Bool
  Returns true if the character is a hexadecimal digit i.e. in the range
  [0-9][a-f][A-F].

  Totality: total
  Visibility: public export
isOctDigit : Bits8 -> Bool
  Returns true if the character is an octal digit.

  Totality: total
  Visibility: public export
isControl : Bits8 -> Bool
  Returns true if the character is a control ASCII character.

  Totality: total
  Visibility: public export
isDot : Bits8 -> Bool
  Returns true if the character equal the '.' ASCII character

  Totality: total
  Visibility: public export
isComma : Bits8 -> Bool
  Returns true if the character equal the ',' ASCII character

  Totality: total
  Visibility: public export
fromBitDigit : Bits8 -> Maybe Nat
  Try to convert a bit digit ('0' or '1') to
  the natural number `0` or `1`.

  Totality: total
  Visibility: public export
fromOctDigit : Bits8 -> Maybe Nat
  Try to convert an ocatal digit to
  the corresponding natural number.

  Totality: total
  Visibility: public export
fromDigit : Bits8 -> Maybe Nat
  Try to convert a decimal digit to
  the corresponding natural number.
  
  Implementation note: Profiling showed that a direct
  pattern match on the input is considerable faster
  than using subtraction together with `isDigit`.

  Totality: total
  Visibility: public export
fromHexDigit : Bits8 -> Maybe Nat
  Try to convert a hexadecimal digit to
  the corresponding natural number.

  Totality: total
  Visibility: public export