Idris2Doc : Data.Int.Order

Data.Int.Order

Implementation of ordering relations for the primitive type `Int`
This is full of tricks as `Int` is a primitive type that can only
be interacted with using either literals or built-in functions.
The exported interface should however be safe.

EQ_not_GT : EQ a b -> Not (GT a b)

Totality: total

EQ_not_LT : EQ a b -> Not (LT a b)

Totality: total

GT : Int -> Int -> Type

  GT is defined in terms of LT to avoid code duplication

Totality: total

GTE : Int -> Int -> Type

  GTE is defined in terms of LTE to avoid code duplication

Totality: total

GT_not_EQ : GT a b -> Not (EQ a b)

Totality: total

GT_not_LT : GT a b -> Not (LT a b)

Totality: total

LT_not_EQ : LT a b -> Not (EQ a b)

Totality: total

LT_not_GT : LT a b -> Not (GT a b)

Totality: total

decide_LTE_GT : (a : Int) -> (b : Int) -> Either (LTE a b) (GT a b)

  Any pair of Ints is related either via LTE or GT

Totality: total

decide_LT_GTE : (a : Int) -> (b : Int) -> Either (LT a b) (GTE a b)

  Any pair of Ints is related either via LT or GTE

Totality: total

pred_LT_LTE : LT a b -> LTE a (b - 1)

  Subtracting one to a strictly larger Int, yields a larger Int

Totality: total

strictRefl : a = b -> Lazy c -> c

  Pattern-match on an equality proof so that the second argument to
  strictRefl is only returned once the first is canonical.

Totality: total

sucBounded : LT a b -> LT a (a + 1)

  Adding one to an Int yields a strictly larger one,
  provided there is no overflow

Totality: total

suc_LT_LTE : LT a b -> LTE (a + 1) b

  Adding one to a strictly smaller Int, yields a smaller Int

Totality: total

trans_EQ_LT : EQ a b -> LT b c -> LT a c

Totality: total

trans_LT_EQ : LT a b -> EQ b c -> LT a c

Totality: total

trichotomous : (a : Int) -> (b : Int) -> Trichotomous LT EQ GT a b

  Any pair of Ints is related either via LT, EQ, or GT

Totality: total