Stdlib.Data.Int.Base
Contents
builtin int type IntSource#
Inductive integers. I.e. whole numbers that can be positive, zero, or negative.
Constructors
ofNat n represents the integer n
negSuc n represents the integer -(n + 1)
toNat : Int -> NatSource#
Converts an Int to a Nat. If the Int is negative, it returns zero.
builtin int-nonneg nonNeg : Int -> BoolSource#
Non-negative predicate for Ints.
builtin int-sub-nat intSubNat (n m : Nat) : IntSource#
Subtraction for Nats.
builtin int-plus + : Int -> Int -> IntSource#
Addition for Ints.
builtin int-neg-nat negNat : Nat -> IntSource#
Negation for Nats.
builtin int-neg neg : Int -> IntSource#
Negation for Ints.
builtin int-mul * : Int -> Int -> IntSource#
Multiplication for Ints.
builtin int-sub - (n m : Int) : IntSource#
Subtraction for Ints.
builtin int-div div : Int -> Int -> IntSource#
Division for Ints.
builtin int-mod mod : Int -> Int -> IntSource#
Modulo for Ints.
abs : Int -> NatSource#
Absolute value
