Idris2Doc : Data.Refined.Integer

Data.Refined.Integer

(source)
Reexports
import public Data.Prim.Integer
import public Data.Refined.Core
Definitions
0 LessThan : Integer -> Integer -> 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```.

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

  Totality: total
  Visibility: public export
0 GreaterThan : Integer -> Integer -> 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```.

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

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

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

  Totality: total
  Visibility: public export
0 widen : FromTo m n x -> {auto 0 _ : m2 <= m} -> {auto 0 _ : n <= n2} -> FromTo m2 n2 x
  Totality: total
  Visibility: export
0 widen' : Between m n x -> {auto 0 _ : m2 <= m} -> {auto 0 _ : n <= n2} -> Between m2 n2 x
  Totality: total
  Visibility: export