Idris2Doc : Data.Refined.Char

Data.Refined.Char

(source)
Reexports
import public Data.Prim.Char
import public Data.Refined.Core
Definitions
0 LessThan : Char -> Char -> Type
  `LessThan m n` is an alias for `n < m`.
  
  This is useful when defining ranges such as
  `From 2 && LessThan 10`, but it gives the wrong idea when used in
  infix notation. So, don't do this: ```x `LessThan` 10```.

  Visibility: public export
0 To : Char -> Char -> Type
  `From m n` is an alias for `n <= m`.

  Visibility: public export
0 GreaterThan : Char -> Char -> Type
  `GreaterThan m n` is an alias for `m < n`.
  
  This is useful when defining ranges such as
  `From 2 && LessThan 10`, but it gives the wrong idea when used in
  infix notation. So, don't do this: ```x `GreaterThan` 10```.

  Visibility: public export
0 From : Char -> Char -> Type
  `From m n` is an alias for `m <= n`.

  Visibility: public export
0 FromTo : Char -> Char -> Char -> Type
  `FromTo m n` is an alias for `From m && To n`.

  Visibility: public export
0 Between : Char -> Char -> Char -> Type
  `Between m n` is an alias for `GreaterThan m && LessThan n`.

  Visibility: public export
0 widen : FromTo m n x -> {auto 0 _ : m2 <= m} -> {auto 0 _ : n <= n2} -> FromTo m2 n2 x
  Visibility: export
0 widen' : Between m n x -> {auto 0 _ : m2 <= m} -> {auto 0 _ : n <= n2} -> Between m2 n2 x
  Visibility: export
0 Ascii : Char -> Type
  Visibility: public export
0 Printable : Char -> Type
  Visibility: public export
0 PrintableAscii : Char -> Type
  Visibility: public export
0 Upper : Char -> Type
  Visibility: public export
0 Lower : Char -> Type
  Visibility: public export
0 Binit : Char -> Type
  Visibility: public export
0 Octit : Char -> Type
  Visibility: public export
0 Digit : Char -> Type
  Visibility: public export
0 Hexit : Char -> Type
  Visibility: public export
0 Alpha : Char -> Type
  Visibility: public export
0 AlphaNum : Char -> Type
  Visibility: public export