Text.ILex.Char.UTF8

Definitions

isAscii : Bits8 -> Bool

  True if the given byte is an ASCII character (in the range `[0..127]`).

Totality: total
Visibility: export

isStartByte : Bits8 -> Bool

  True, if the given byte is the first byte
  of an UTF-8 encoded code point.

Totality: total
Visibility: export

record Codepoint : Type

  A unicode code point encoded as a list of up to
  four bytes.

Totality: total
Visibility: public export
Constructor: 

CP : (0 len : Nat) -> Vect (S len) Bits8 -> Codepoint

Projections:

.bytes : ({rec:0} : Codepoint) -> Vect (S (len {rec:0})) Bits8

0 .len : Codepoint -> Nat

0 .len : Codepoint -> Nat

Totality: total
Visibility: public export

0 len : Codepoint -> Nat

Totality: total
Visibility: public export

.bytes : ({rec:0} : Codepoint) -> Vect (S (len {rec:0})) Bits8

Totality: total
Visibility: public export

bytes : ({rec:0} : Codepoint) -> Vect (S (len {rec:0})) Bits8

Totality: total
Visibility: public export

record Span : Type

  A range of unicode codepoints that take up the same number
  of bytes when UTF-8 encoded.

Totality: total
Visibility: export
Constructor: 

SP : Vect (S len) Bits8 -> Vect (S len) Bits8 -> Span

Projections:

.c1 : ({rec:0} : Span) -> Vect (S (len {rec:0})) Bits8

.c2 : ({rec:0} : Span) -> Vect (S (len {rec:0})) Bits8

0 .len : Span -> Nat

toByteRanges : Set32 -> RExp8 True

Totality: total
Visibility: export

toUTF8 : (RExp b, a) -> (RExp8 b, a)

Totality: total
Visibility: export