Data.Prim.Char

Reexports

Definitions

data (<) : Char -> Char -> Type

  Witness that `m < n === True`.

Totality: total
Visibility: export
Constructor: 

LT : (0 _ : m < n = True) -> m < n

Hints:

(0 _ : m < n = True) -> m < n

Total Char (<)

WellFounded Char (<)

Fixity Declaration: infix operator, level 6

0 mkLT : (0 _ : m < n = True) -> m < n

  Contructor for `(<)`.
  
  This can only be used in an erased context.

Totality: total
Visibility: export

0 runLT : m < n -> m < n = True

  Extractor for `(<)`.
  
  This can only be used in an erased context.

Totality: total
Visibility: export

strictLT : (0 _ : m < n) -> Lazy c -> c

  We don't trust values of type `(<)` too much,
  so we use this when creating magical results.

Totality: total
Visibility: export

0 (>) : Char -> Char -> Type

  Flipped version of `(<)`.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6

0 (<=) : Char -> Char -> Type

  `m <= n` mean that either `m < n` or `m === n` holds.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6

0 (>=) : Char -> Char -> Type

  Flipped version of `(<=)`.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6

0 (/=) : Char -> Char -> Type

  `m /= n` mean that either `m < n` or `m > n` holds.

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6

comp : (m : Char) -> (n : Char) -> Trichotomy (<) m n

Totality: total
Visibility: export

MinChar : Char

  Lower bound of `Char`

Totality: total
Visibility: public export

0 GTE_MinChar : (m : Char) -> m >= MinChar

  `m >= MinChar` for all `m` of type `Char`.

Totality: total
Visibility: export

0 Not_LT_MinChar : m < MinChar -> Void

  Not value of type `Char` is less than `MinChar`.

Totality: total
Visibility: export

accessLT : (m : Char) -> Accessible (<) m

  Every value of type `Char` is accessible with relation
  to `(<)`.

Totality: total
Visibility: export