Data.INTEGER

Definitions

data INTEGER : Type

Totality: total
Visibility: public export
Constructors:

Z : INTEGER

PS : Nat -> INTEGER

NS : Nat -> INTEGER

Hints:

Cast Nat INTEGER

Cast Integer INTEGER

Cast INTEGER Integer

Neg INTEGER

Num INTEGER

Show INTEGER

add : INTEGER -> INTEGER -> INTEGER

Totality: total
Visibility: public export

mult : INTEGER -> INTEGER -> INTEGER

Totality: total
Visibility: public export

plusZeroRightNeutral : (m : INTEGER) -> m + Z = m

Totality: total
Visibility: export

plusCommutative : (m : INTEGER) -> (n : INTEGER) -> m + n = n + m

Totality: total
Visibility: export

castPlus : (m : Nat) -> (n : Nat) -> the INTEGER (cast (m + n)) = cast m + cast n

Totality: total
Visibility: export

unfoldPS : (m : Nat) -> PS m = 1 + cast m

Totality: total
Visibility: export

unfoldNS : (m : Nat) -> NS m = -1 - cast m

Totality: total
Visibility: export

difference : Nat -> Nat -> INTEGER

Totality: total
Visibility: export

differenceZeroRight : (n : Nat) -> difference n 0 = cast n

Totality: total
Visibility: export

minusSuccSucc : (m : Nat) -> (n : Nat) -> the INTEGER (cast (S m) - cast (S n)) = cast m - cast n

Totality: total
Visibility: export

unfoldDifference : (m : Nat) -> (n : Nat) -> difference m n = cast m - cast n

Totality: total
Visibility: export

negateInvolutive : (m : INTEGER) -> negate (negate m) = m

Totality: total
Visibility: export

negatePlus : (m : INTEGER) -> (n : INTEGER) -> negate (m + n) = negate m + negate n

Totality: total
Visibility: export

negateDifference : (m : Nat) -> (n : Nat) -> negate (difference m n) = difference n m

Totality: total
Visibility: export

minusZeroRight : (m : INTEGER) -> m - Z = m

Totality: total
Visibility: export

plusInverse : (m : INTEGER) -> m - m = Z

Totality: total
Visibility: export

plusAssociative : (m : INTEGER) -> (n : INTEGER) -> (p : INTEGER) -> m + (n + p) = (m + n) + p

Totality: total
Visibility: export