Idris2Doc : Text.ILex.Char.Range

Text.ILex.Char.Range

(source)
Definitions
interface WithBounds : Type -> Type
  Parameters: a
Constraints: Ord a
Methods:
  
minBound : a
  
maxBound : a

Implementations:
  
WithBounds Bits8
  
WithBounds Bits16
  
WithBounds Bits32
  
WithBounds Bits64
minBound : WithBounds a => a
  Totality: total
  Visibility: public export
maxBound : WithBounds a => a
  Totality: total
  Visibility: public export
data RangeOf : Type -> Type
  A range of unicode code points.
  
  Actually, it's a range of 32-bit numbers, but we use it for describing
  ranges of codepoints in this library.

  Totality: total
  Visibility: export
  Constructors:
  
Empty : RangeOf t
  
Rng : t -> t -> RangeOf t

  Hints:
  
Eq t => Eq (RangeOf t)
  
Ord t => Ord (RangeOf t)
  
Show t => Show (RangeOf t)
0 Range8 : Type
  Totality: total
  Visibility: public export
0 Range32 : Type
  Totality: total
  Visibility: public export
empty : RangeOf t
  The empty range of codepoints.

  Totality: total
  Visibility: export
singleton : t -> RangeOf t
  A range containing a single value

  Totality: total
  Visibility: export
isEmpty : RangeOf t -> Bool
  Totality: total
  Visibility: export
range : Ord t => t -> t -> RangeOf t
  Generates a new range from `x` to `y` if `x` is strictly
  smaller than `y`. Otherwise, the empty range is returned.

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

  Totality: total
  Visibility: export
overlap : Ord t => RangeOf t -> RangeOf t -> Bool
  True if the two ranges overlap

  Totality: total
  Visibility: export
span : Ord t => RangeOf t -> RangeOf t -> RangeOf t
  Spans the range from the lowest to the largest bound of the two ranges.

  Totality: total
  Visibility: export
intersection : Ord t => RangeOf t -> RangeOf t -> RangeOf t
  Intersection of two ranges, if any.

  Totality: total
  Visibility: export
adjacent : Ord t => Neg t => RangeOf t -> RangeOf t -> Bool
  True if the two ranges are adjacent, that is, the upper bound
  of one range is one less than the lower bound of the other.

  Totality: total
  Visibility: export
union : Ord t => Neg t => RangeOf t -> RangeOf t -> Either (RangeOf t) (RangeOf t, RangeOf t)
  Union of the ranges.
  
  If there are two results then they are guaranteed to be non-empty,
  have a non-empty gap in between, and are in ascending order

  Totality: total
  Visibility: export
difference : Ord t => Neg t => RangeOf t -> RangeOf t -> Either (RangeOf t) (RangeOf t, RangeOf t)
  Returns the result of subtracting the second range from the first.
  
  If there are two results then they are guaranteed to be non-empty,
  have a non-empty gap in between, and are in ascending order

  Totality: total
  Visibility: export
codepoint : Range32
  The range of all unicode code points.

  Totality: total
  Visibility: export
surrogate : Range32
  The range of surrogate pairs.

  Totality: total
  Visibility: export
charRange : Char -> Char -> Range32
  A range corresponding to a pair of characters.

  Totality: total
  Visibility: export
fullRange : WithBounds t => RangeOf t
  The full range.  All 32 bit values are within it.

  Totality: total
  Visibility: export
isFull : WithBounds t => RangeOf t -> Bool
  A range is full if it contains every possible value.

  Totality: total
  Visibility: export
lowerBound : WithBounds t => RangeOf t -> t
  Totality: total
  Visibility: export
upperBound : WithBounds t => RangeOf t -> t
  Totality: total
  Visibility: export