# Documentation

Std.Data.Int.Basic

-[n+1] is suggestive notation for negSucc n, which is the second constructor of Int for making strictly negative numbers by mapping n : Nat to -(n + 1).

Equations
• One or more equations did not get rendered due to their size.
def Int.sign :

Returns the "sign" of the integer as another integer: 1 for positive numbers, -1 for negative numbers, and 0 for 0.

Equations
• = match x with | => 1 | => 0 | => -1

## toNat' #

• If n : Nat, then int.toNat' n = some n
• If n : Int is negative, then int.toNat' n = none.
Equations
• = match x with | => some n | => none

## Quotient and remainder #

There are three main conventions for integer division, referred here as the E, F, T rounding conventions. All three pairs satisfy the identity x % y + (x / y) * y = x unconditionally, and satisfy x / 0 = 0 and x % 0 = x.

### E-rounding division #

This pair satisfies 0 ≤ mod x y < natAbs y≤ mod x y < natAbs y for y ≠ 0≠ 0.

def Int.ediv :

Integer division. This version of Int.div uses the E-rounding convention (euclidean division), in which Int.emod x y satisfies 0 ≤ mod x y < natAbs y≤ mod x y < natAbs y for y ≠ 0≠ 0 and Int.ediv is the unique function satisfying emod x y + (ediv x y) * y = x.

Equations
• One or more equations did not get rendered due to their size.
def Int.emod :

Integer modulus. This version of Int.mod uses the E-rounding convention (euclidean division), in which Int.emod x y satisfies 0 ≤ emod x y < natAbs y≤ emod x y < natAbs y for y ≠ 0≠ 0 and Int.ediv is the unique function satisfying emod x y + (ediv x y) * y = x.

Equations

### F-rounding division #

This pair satisfies fdiv x y = floor (x / y).

def Int.fdiv :

Integer division. This version of Int.div uses the F-rounding convention (flooring division), in which Int.fdiv x y satisfies fdiv x y = floor (x / y) and Int.fmod is the unique function satisfying fmod x y + (fdiv x y) * y = x.

Equations
• One or more equations did not get rendered due to their size.
def Int.fmod :

Integer modulus. This version of Int.mod uses the F-rounding convention (flooring division), in which Int.fdiv x y satisfies fdiv x y = floor (x / y) and Int.fmod is the unique function satisfying fmod x y + (fdiv x y) * y = x.

Equations
• One or more equations did not get rendered due to their size.

### T-rounding division #

This pair satisfies div x y = round_to_zero (x / y). Int.div and Int.mod are defined in core lean.

instance Int.instDivInt_1 :

Core Lean provides instances using T-rounding division, i.e. Int.div and Int.mod. We override these here.

Equations

## gcd #

def Int.gcd (m : Int) (n : Int) :

Computes the greatest common divisor of two integers, as a Nat.

Equations

## divisibility #

instance Int.instDvdInt :

Divisibility of integers. a ∣ b∣ b (typed as \|) says that there is some c such that b = a * c.

Equations