Text.ILex.Util

(source)

Definitions

decimaldigit : Bits8 -> Integer

Totality: total
Visibility: export

hexdigit : Bits8 -> Integer

Totality: total
Visibility: export

binaryBV : IBuffer n -> Integer -> (k : Nat) -> Ix k n => Integer

Totality: total
Visibility: export

binarySepBV : IBuffer n -> Integer -> (k : Nat) -> Ix k n => Integer

Totality: total
Visibility: export

octalBV : IBuffer n -> Integer -> (k : Nat) -> Ix k n => Integer

Totality: total
Visibility: export

octalSepBV : IBuffer n -> Bits8 -> Integer -> (k : Nat) -> Ix k n => Integer

Totality: total
Visibility: export

decimalBV : IBuffer n -> Integer -> (k : Nat) -> Ix k n => Integer

Totality: total
Visibility: export

decimalSepBV : IBuffer n -> Bits8 -> Integer -> (k : Nat) -> Ix k n => Integer

Totality: total
Visibility: export

hexadecimalBV : IBuffer n -> Integer -> (k : Nat) -> Ix k n => Integer

Totality: total
Visibility: export

hexadecimalSepBV : IBuffer n -> Bits8 -> Integer -> (k : Nat) -> Ix k n => Integer

Totality: total
Visibility: export

integerBV : IBuffer n -> (k : Nat) -> Ix k n => Integer

Totality: total
Visibility: export

binary : ByteString -> Integer

  Converts a string of binary digits to an integer

Totality: total
Visibility: export

binarySep : ByteString -> Integer

  Converts a string of binary digits containing optional
  separators to an integer `0010_0011_1110_0011.
  
  Such integer literals are supported by Idris as well as TOML,
  for instance:

Totality: total
Visibility: export

octal : ByteString -> Integer

  Converts a string of octal digits to an integer

Totality: total
Visibility: export

octalSep : Bits8 -> ByteString -> Integer

  Converts a string of octal digits containing optional
  separators to an integer `077_334`.
  
  Such integer literals are supported by Idris as well as TOML,
  for instance:

Totality: total
Visibility: export

decimal : ByteString -> Integer

  Converts a string of decimal digits to an integer

Totality: total
Visibility: export

decimalSep : Bits8 -> ByteString -> Integer

  Converts a string of decimal digits containing optional
  separators to an integer `177_934`.
  
  Such integer literals are supported by Idris as well as TOML,
  for instance:

Totality: total
Visibility: export

hexadecimal : ByteString -> Integer

  Converts a string of decimal digits to an integer

Totality: total
Visibility: export

hexadecimalSep : Bits8 -> ByteString -> Integer

  Converts a string of decimal digits containing optional
  separators to an integer `177_934`.
  
  Such integer literals are supported by Idris as well as TOML,
  for instance:

Totality: total
Visibility: export

integer : ByteString -> Integer

  Converts an integer literal with optional sign prefix
  to an integer.

Totality: total
Visibility: export

maybeList : SnocList a -> Maybe (List a)

  Utility for converting a snoc list into a list.
  
  This is useful when streaming chunks of data and emitting
  all the accumulated values of a single chunk.

Totality: total
Visibility: export

snocPack : SnocList String -> String

  Concatenates the strings accumulated in a snoc list.
  
  This is a utility often used when lexing or parsing
  string literals that support various kinds of escape
  sequences.

Totality: total
Visibility: export