Idris2Doc : Text.ILex.Char.Set

Text.ILex.Char.Set

(source)
Reexports
import public Text.ILex.Char.Range
Definitions
record SetOf : Type -> Type
  A set of unicode points (actually, a set of 32-bit characters)
  represented internally as an ordered list of disjoint character
  ranges.

  Totality: total
  Visibility: export
  Constructor: 
S : List (RangeOf t) -> SetOf t

  Projection: 
.ranges_ : SetOf t -> List (RangeOf t)
  A list of ordered, non-overlapping, non-adjacent, and non-empty ranges

  Hints:
  
Eq t => Eq (SetOf t)
  
Ord t => Ord (SetOf t)
  
Show t => Show (SetOf t)
0 Set8 : Type
  Totality: total
  Visibility: public export
0 Set32 : Type
  Totality: total
  Visibility: public export
ranges : SetOf t -> List (RangeOf t)
  Returns the inner list of ranges of a character set.
  
  The returned list is sorted and the ranges it contains are disjoint
  and non-adjacent.

  Totality: total
  Visibility: export
empty : SetOf t
  The empty set of codepoints.

  Totality: total
  Visibility: export
singleton : t -> SetOf t
  The set holding only the given codepoint.

  Totality: total
  Visibility: export
range : RangeOf t -> SetOf t
  The set holding all characters in the given range.

  Totality: total
  Visibility: export
isEmpty : SetOf t -> Bool
  `True` if the character set is empty.

  Totality: total
  Visibility: export
has : Ord t => SetOf t -> t -> Bool
  True if the value is within the set.

  Totality: total
  Visibility: export
rangeSet : WithBounds t => Neg t => List (RangeOf t) -> SetOf t
  Creates a character set from the given list of ranges.
  
  The ranges are first sorted and overlapping or adjacent ranges
  are unified before wrapping them up.

  Totality: total
  Visibility: export
union : WithBounds t => Neg t => SetOf t -> SetOf t -> SetOf t
  Set union.

  Totality: total
  Visibility: export
intersection : WithBounds t => Neg t => SetOf t -> SetOf t -> SetOf t
  Set intersection.

  Totality: total
  Visibility: export
negation : WithBounds t => Neg t => SetOf t -> SetOf t
  Set negation.

  Totality: total
  Visibility: export
difference : WithBounds t => Neg t => SetOf t -> SetOf t -> SetOf t
  Set difference.

  Totality: total
  Visibility: export
chars : String -> Set32
  The set holding the codepoints (characters) in the given
  string.

  Totality: total
  Visibility: export
fullSet : WithBounds t => SetOf t
  The set holding all 32-bit values.

  Totality: total
  Visibility: export
isFull : WithBounds t => SetOf t -> Bool
  `True` if this set holds all 32-bit values.

  Totality: total
  Visibility: export
charRange : Char -> Char -> Set32
  A range of unicode code points.

  Totality: total
  Visibility: export
lower : Set32
  The set of lower-case letters.

  Totality: total
  Visibility: export
upper : Set32
  The set of upper-case letters.

  Totality: total
  Visibility: export
alpha : Set32
  The set of letters.

  Totality: total
  Visibility: export
digit : Set32
  The set of digits.

  Totality: total
  Visibility: export
posdigit : Set32
  The set of positive digits.

  Totality: total
  Visibility: export
alphaNum : Set32
  The set of digits and letters.

  Totality: total
  Visibility: export
control : Set32
  The set of control characters.

  Totality: total
  Visibility: export
printable : Set32
  The set of printable characters.
  
  This is the negation of `control`.

  Totality: total
  Visibility: export
ascii : Set32
  The set of ASCII characters.

  Totality: total
  Visibility: export
printableAscii : Set32
  The set of non-control ASCII characters.

  Totality: total
  Visibility: export
nl : Set32
  The newline character ('\n')

  Totality: total
  Visibility: export
unicode : Set32
  The set of unicode code points (minus surrogate pairs).

  Totality: total
  Visibility: export