Idris2Doc : Data.Nat

Data.Nat

dataCmpNat : Nat -> Nat -> Type
Totality: total
Constructors:
CmpLT : (y : Nat) -> CmpNatx (x+Sy)
CmpEQ : CmpNatxx
CmpGT : (x : Nat) -> CmpNat (y+Sx) y
GT : Nat -> Nat -> Type
Totality: total
GTE : Nat -> Nat -> Type
Totality: total
dataIsSucc : Nat -> Type
Totality: total
Constructor: 
ItIsSucc : IsSucc (Sn)
LT : Nat -> Nat -> Type
Totality: total
dataLTE : Nat -> Nat -> Type
Totality: total
Constructors:
LTEZero : LTE0right
LTESucc : LTEleftright -> LTE (Sleft) (Sright)
LTEImpliesNotGT : LTEab -> Not (GTab)
Totality: total
LTImpliesNotGTE : LTab -> Not (GTEab)
Totality: total
dataNonZero : 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 (Sx)
dataNotBothZero : Nat -> Nat -> Type
Totality: total
Constructors:
LeftIsNotZero : NotBothZero (Sn) m
RightIsNotZero : NotBothZeron (Sm)
SIsNotZ : Not (Sx = 0)
Totality: total
cmp : (x : Nat) -> (y : Nat) -> CmpNatxy
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 _ : NonZeroy) -> Nat
divNat : Nat -> Nat -> Nat
divNatNZ : Nat -> (y : Nat) -> (0 _ : NonZeroy) -> Nat
Totality: total
divmod' : Nat -> Nat -> Nat -> (Nat, Nat)
Totality: total
divmodNatNZ : Nat -> (y : Nat) -> (0 _ : NonZeroy) -> (Nat, Nat)
Totality: total
eqSucc : (0 left : Nat) -> (0 right : Nat) -> left = right -> Sleft = Sright
Totality: total
fromLteSucc : LTE (Sm) (Sn) -> LTEmn
Totality: total
gcd : (a : Nat) -> (b : Nat) -> NotBothZeroab => Nat
gt : Nat -> Nat -> Bool
Totality: total
gtReflectsGT : (k : Nat) -> (n : Nat) -> gtkn = True -> GTkn
Totality: total
gte : Nat -> Nat -> Bool
Totality: total
gteReflectsGTE : (k : Nat) -> (n : Nat) -> gtekn = True -> GTEkn
Totality: total
hyper : Nat -> Nat -> Nat -> Nat
Totality: total
isGT : (m : Nat) -> (n : Nat) -> Dec (GTmn)
Totality: total
isGTE : (m : Nat) -> (n : Nat) -> Dec (GTEmn)
Totality: total
isItSucc : (n : Nat) -> Dec (IsSuccn)
Totality: total
isLT : (m : Nat) -> (n : Nat) -> Dec (LTmn)
Totality: total
isLTE : (m : Nat) -> (n : Nat) -> Dec (LTEmn)
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) -> ltkn = True -> LTkn
Totality: total
lte : Nat -> Nat -> Bool
Totality: total
lteAddRight : (n : Nat) -> LTEn (n+m)
Totality: total
lteReflectsLTE : (k : Nat) -> (n : Nat) -> ltekn = True -> LTEkn
Totality: total
lteSuccLeft : LTE (Sn) m -> LTEnm
Totality: total
lteSuccRight : LTEnm -> LTEn (Sm)
Totality: total
maximum : Nat -> Nat -> Nat
Totality: total
maximumAssociative : (l : Nat) -> (c : Nat) -> (r : Nat) -> maximuml (maximumcr) = maximum (maximumlc) r
Totality: total
maximumCommutative : (l : Nat) -> (r : Nat) -> maximumlr = maximumrl
Totality: total
maximumIdempotent : (n : Nat) -> maximumnn = n
Totality: total
maximumSuccSucc : (left : Nat) -> (right : Nat) -> S (maximumleftright) = maximum (Sleft) (Sright)
Totality: total
maximumZeroNLeft : (left : Nat) -> maximumleft0 = left
Totality: total
minimum : Nat -> Nat -> Nat
Totality: total
minimumAssociative : (l : Nat) -> (c : Nat) -> (r : Nat) -> minimuml (minimumcr) = minimum (minimumlc) r
Totality: total
minimumCommutative : (l : Nat) -> (r : Nat) -> minimumlr = minimumrl
Totality: total
minimumIdempotent : (n : Nat) -> minimumnn = n
Totality: total
minimumSuccSucc : (left : Nat) -> (right : Nat) -> minimum (Sleft) (Sright) = S (minimumleftright)
Totality: total
minimumZeroZeroLeft : (left : Nat) -> minimumleft0 = 0
Totality: total
minusLtMonotone : LTmn -> LTpn -> LT (minusmp) (minusnp)
Totality: total
minusLteMonotone : LTEmn -> LTE (minusmp) (minusnp)
Totality: total
minusMinusMinusPlus : (left : Nat) -> (centre : Nat) -> (right : Nat) -> minus (minusleftcentre) right = minusleft (centre+right)
Totality: total
minusOneSuccN : (n : Nat) -> 1 = minus (Sn) n
Totality: total
minusPlus : (m : Nat) -> minus (plusmn) m = n
Totality: total
minusPlusZero : (n : Nat) -> (m : Nat) -> minusn (n+m) = 0
Totality: total
minusPos : LTmn -> LT0 (minusnm)
Totality: total
minusSuccOne : (n : Nat) -> minus (Sn) 1 = n
Totality: total
minusSuccSucc : (left : Nat) -> (right : Nat) -> minus (Sleft) (Sright) = minusleftright
Totality: total
minusZeroLeft : (right : Nat) -> minus0right = 0
Totality: total
minusZeroN : (n : Nat) -> 0 = minusnn
Totality: total
minusZeroRight : (left : Nat) -> minusleft0 = 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 _ : NonZeroy) -> 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) -> minusleftcentre*right = minus (left*right) (centre*right)
Totality: total
multDistributesOverMinusRight : (left : Nat) -> (centre : Nat) -> (right : Nat) -> left*minuscentreright = 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) -> Sleft*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*Sright = left+ (left*right)
Totality: total
multZeroLeftZero : (right : Nat) -> 0*right = 0
Totality: total
multZeroRightZero : (left : Nat) -> left*0 = 0
Totality: total
notLTEImpliesGT : Not (LTEab) -> GTab
Totality: total
notLTImpliesGTE : Not (LTab) -> GTEab
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 : LTEmn -> LTEpq -> LTE (m+p) (n+q)
Totality: total
plusLteMonotoneLeft : (p : Nat) -> (q : Nat) -> (r : Nat) -> LTEqr -> LTE (p+q) (p+r)
Totality: total
plusLteMonotoneRight : (p : Nat) -> (q : Nat) -> (r : Nat) -> LTEqr -> LTE (q+p) (r+p)
Totality: total
plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) -> minus (left+right) (left+right') = minusrightright'
Totality: total
plusMinusLte : (n : Nat) -> (m : Nat) -> LTEnm -> minusmn+n = m
Totality: total
plusOneSucc : (right : Nat) -> 1+right = Sright
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+Sright
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 (Sl) l = Sl
Totality: total
sucMaxR : (l : Nat) -> maximuml (Sl) = Sl
Totality: total
sucMinL : (l : Nat) -> minimum (Sl) l = l
Totality: total
sucMinR : (l : Nat) -> minimuml (Sl) = l
Totality: total
succInjective : (0 left : Nat) -> (0 right : Nat) -> Sleft = Sright -> left = right
Totality: total
succNotLTEpred : Not (LTE (Sx) x)
Totality: total
succNotLTEzero : Not (LTE (Sm) 0)
Totality: total
zeroMultEitherZero : (a : Nat) -> (b : Nat) -> a*b = 0 -> Either (a = 0) (b = 0)
Totality: total