Idris2Doc : Data.Nat

Data.Nat

data CmpNat : Nat -> Nat -> Type
  Totality: total
  Constructors:
  
CmpLT : (y : Nat) -> CmpNat x (x + S y)
  
CmpEQ : CmpNat x x
  
CmpGT : (x : Nat) -> CmpNat (y + S x) y
GT : Nat -> Nat -> Type
  Totality: total
GTE : Nat -> Nat -> Type
  Totality: total
data IsSucc : Nat -> Type
  Totality: total
  Constructor: 
ItIsSucc : IsSucc (S n)
LT : Nat -> Nat -> Type
  Totality: total
data LTE : Nat -> Nat -> Type
  Totality: total
  Constructors:
  
LTEZero : LTE 0 right
  
LTESucc : LTE left right -> LTE (S left) (S right)
LTEImpliesNotGT : LTE a b -> Not (GT a b)
  Totality: total
LTImpliesNotGTE : LT a b -> Not (GTE a b)
  Totality: total
data NonZero : Nat -> Type
  A definition of non-zero with a better behaviour than `Not (x = Z)`
  This is amenable to proof search and `NonZero Z` is more readily
  detected as impossible by Idris

  Totality: total
  Constructor: 
SIsNonZero : NonZero (S x)
data NotBothZero : Nat -> Nat -> Type
  Totality: total
  Constructors:
  
LeftIsNotZero : NotBothZero (S n) m
  
RightIsNotZero : NotBothZero n (S m)
SIsNotZ : Not (S x = 0)
  Totality: total
cmp : (x : Nat) -> (y : Nat) -> CmpNat x y
  Totality: total
div' : Nat -> Nat -> Nat -> Nat
  Auxiliary function:
  div' fuel a b = a `div` (S b)
  assuming we have enough fuel

  Totality: total
divCeil : Nat -> Nat -> Nat
  
divCeilNZ : Nat -> (y : Nat) -> (0 _ : NonZero y) -> Nat
  
divNat : Nat -> Nat -> Nat
  
divNatNZ : Nat -> (y : Nat) -> (0 _ : NonZero y) -> Nat
  Totality: total
divmod' : Nat -> Nat -> Nat -> (Nat, Nat)
  Totality: total
divmodNatNZ : Nat -> (y : Nat) -> (0 _ : NonZero y) -> (Nat, Nat)
  Totality: total
eqSucc : (0 left : Nat) -> (0 right : Nat) -> left = right -> S left = S right
  Totality: total
fromLteSucc : LTE (S m) (S n) -> LTE m n
  Totality: total
gcd : (a : Nat) -> (b : Nat) -> NotBothZero a b => Nat
  
gt : Nat -> Nat -> Bool
  Totality: total
gtReflectsGT : (k : Nat) -> (n : Nat) -> gt k n = True -> GT k n
  Totality: total
gte : Nat -> Nat -> Bool
  Totality: total
gteReflectsGTE : (k : Nat) -> (n : Nat) -> gte k n = True -> GTE k n
  Totality: total
hyper : Nat -> Nat -> Nat -> Nat
  Totality: total
isGT : (m : Nat) -> (n : Nat) -> Dec (GT m n)
  Totality: total
isGTE : (m : Nat) -> (n : Nat) -> Dec (GTE m n)
  Totality: total
isItSucc : (n : Nat) -> Dec (IsSucc n)
  Totality: total
isLT : (m : Nat) -> (n : Nat) -> Dec (LT m n)
  Totality: total
isLTE : (m : Nat) -> (n : Nat) -> Dec (LTE m n)
  Totality: total
isSucc : Nat -> Bool
  Totality: total
isZero : Nat -> Bool
  Totality: total
lcm : Nat -> Nat -> Nat
  
lt : Nat -> Nat -> Bool
  Totality: total
ltReflectsLT : (k : Nat) -> (n : Nat) -> lt k n = True -> LT k n
  Totality: total
lte : Nat -> Nat -> Bool
  Totality: total
lteAddRight : (n : Nat) -> LTE n (n + m)
  Totality: total
lteReflectsLTE : (k : Nat) -> (n : Nat) -> lte k n = True -> LTE k n
  Totality: total
lteSuccLeft : LTE (S n) m -> LTE n m
  Totality: total
lteSuccRight : LTE n m -> LTE n (S m)
  Totality: total
maximum : Nat -> Nat -> Nat
  Totality: total
maximumAssociative : (l : Nat) -> (c : Nat) -> (r : Nat) -> maximum l (maximum c r) = maximum (maximum l c) r
  Totality: total
maximumCommutative : (l : Nat) -> (r : Nat) -> maximum l r = maximum r l
  Totality: total
maximumIdempotent : (n : Nat) -> maximum n n = n
  Totality: total
maximumSuccSucc : (left : Nat) -> (right : Nat) -> S (maximum left right) = maximum (S left) (S right)
  Totality: total
maximumZeroNLeft : (left : Nat) -> maximum left 0 = left
  Totality: total
minimum : Nat -> Nat -> Nat
  Totality: total
minimumAssociative : (l : Nat) -> (c : Nat) -> (r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r
  Totality: total
minimumCommutative : (l : Nat) -> (r : Nat) -> minimum l r = minimum r l
  Totality: total
minimumIdempotent : (n : Nat) -> minimum n n = n
  Totality: total
minimumSuccSucc : (left : Nat) -> (right : Nat) -> minimum (S left) (S right) = S (minimum left right)
  Totality: total
minimumZeroZeroLeft : (left : Nat) -> minimum left 0 = 0
  Totality: total
minusLtMonotone : LT m n -> LT p n -> LT (minus m p) (minus n p)
  Totality: total
minusLteMonotone : LTE m n -> LTE (minus m p) (minus n p)
  Totality: total
minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) -> minus (minus left centre) right = minus left (centre + right)
  Totality: total
minusOneSuccN : (n : Nat) -> 1 = minus (S n) n
  Totality: total
minusPlus : (m : Nat) -> minus (plus m n) m = n
  Totality: total
minusPlusZero : (n : Nat) -> (m : Nat) -> minus n (n + m) = 0
  Totality: total
minusPos : LT m n -> LT 0 (minus n m)
  Totality: total
minusSuccOne : (n : Nat) -> minus (S n) 1 = n
  Totality: total
minusSuccSucc : (left : Nat) -> (right : Nat) -> minus (S left) (S right) = minus left right
  Totality: total
minusZeroLeft : (right : Nat) -> minus 0 right = 0
  Totality: total
minusZeroN : (n : Nat) -> 0 = minus n n
  Totality: total
minusZeroRight : (left : Nat) -> minus left 0 = left
  Totality: total
mod' : Nat -> Nat -> Nat -> Nat
  Auxiliary function:
  mod' fuel a b = a `mod` (S b)
  assuming we have enough fuel

  Totality: total
modNat : Nat -> Nat -> Nat
  
modNatNZ : Nat -> (y : Nat) -> (0 _ : NonZero y) -> Nat
  Totality: total
multAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * (centre * right) = (left * centre) * right
  Totality: total
multCommutative : (left : Nat) -> (right : Nat) -> left * right = right * left
  Totality: total
multDistributesOverMinusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) -> minus left centre * right = minus (left * right) (centre * right)
  Totality: total
multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * minus centre right = minus (left * centre) (left * right)
  Totality: total
multDistributesOverPlusLeft : (left : Nat) -> (centre : Nat) -> (right : Nat) -> (left + centre) * right = (left * right) + (centre * right)
  Totality: total
multDistributesOverPlusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left * (centre + right) = (left * centre) + (left * right)
  Totality: total
multLeftSuccPlus : (left : Nat) -> (right : Nat) -> S left * right = right + (left * right)
  Totality: total
multOneLeftNeutral : (right : Nat) -> 1 * right = right
  Totality: total
multOneRightNeutral : (left : Nat) -> left * 1 = left
  Totality: total
multRightSuccPlus : (left : Nat) -> (right : Nat) -> left * S right = left + (left * right)
  Totality: total
multZeroLeftZero : (right : Nat) -> 0 * right = 0
  Totality: total
multZeroRightZero : (left : Nat) -> left * 0 = 0
  Totality: total
notLTEImpliesGT : Not (LTE a b) -> GT a b
  Totality: total
notLTImpliesGTE : Not (LT a b) -> GTE a b
  Totality: total
plusAssociative : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left + (centre + right) = (left + centre) + right
  Totality: total
plusCommutative : (left : Nat) -> (right : Nat) -> left + right = right + left
  Totality: total
plusConstantLeft : (left : Nat) -> (right : Nat) -> (c : Nat) -> left = right -> c + left = c + right
  Totality: total
plusConstantRight : (left : Nat) -> (right : Nat) -> (c : Nat) -> left = right -> left + c = right + c
  Totality: total
plusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) -> left + right = left + right' -> right = right'
  Totality: total
plusLeftLeftRightZero : (left : Nat) -> (right : Nat) -> left + right = left -> right = 0
  Totality: total
plusLteMonotone : LTE m n -> LTE p q -> LTE (m + p) (n + q)
  Totality: total
plusLteMonotoneLeft : (p : Nat) -> (q : Nat) -> (r : Nat) -> LTE q r -> LTE (p + q) (p + r)
  Totality: total
plusLteMonotoneRight : (p : Nat) -> (q : Nat) -> (r : Nat) -> LTE q r -> LTE (q + p) (r + p)
  Totality: total
plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) -> minus (left + right) (left + right') = minus right right'
  Totality: total
plusMinusLte : (n : Nat) -> (m : Nat) -> LTE n m -> minus m n + n = m
  Totality: total
plusOneSucc : (right : Nat) -> 1 + right = S right
  Totality: total
plusRightCancel : (left : Nat) -> (left' : Nat) -> (right : Nat) -> left + right = left' + right -> left = left'
  Totality: total
plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right
  Totality: total
plusZeroLeftNeutral : (right : Nat) -> 0 + right = right
  Totality: total
plusZeroRightNeutral : (left : Nat) -> left + 0 = left
  Totality: total
power : Nat -> Nat -> Nat
  Totality: total
pred : Nat -> Nat
  Totality: total
sucMaxL : (l : Nat) -> maximum (S l) l = S l
  Totality: total
sucMaxR : (l : Nat) -> maximum l (S l) = S l
  Totality: total
sucMinL : (l : Nat) -> minimum (S l) l = l
  Totality: total
sucMinR : (l : Nat) -> minimum l (S l) = l
  Totality: total
succInjective : (0 left : Nat) -> (0 right : Nat) -> S left = S right -> left = right
  Totality: total
succNotLTEpred : Not (LTE (S x) x)
  Totality: total
succNotLTEzero : Not (LTE (S m) 0)
  Totality: total
zeroMultEitherZero : (a : Nat) -> (b : Nat) -> a * b = 0 -> Either (a = 0) (b = 0)
  Totality: total