Init.Data.Int.Basic

source

inductive Int :

Type

ofNat: Nat → Int
negSucc: Nat → Int

source

instance instCoeNatInt :

Coe Nat Int

Equations

instCoeNatInt = { coe := Int.ofNat }

source

instance instOfNatInt {n : Nat} :

OfNat Int n

Equations

instOfNatInt = { ofNat := Int.ofNat n }

source

instance Int.instInhabitedInt :

Inhabited Int

Equations

Int.instInhabitedInt = { default := Int.ofNat 0 }

source

def Int.negOfNat :

Nat → Int

Equations

Int.negOfNat _fun_discr = match _fun_discr with | 0 => 0 | Nat.succ m => Int.negSucc m

source

@[extern lean_int_neg]

def Int.neg (n : Int) :

Int

Equations

Int.neg n = match n with | Int.ofNat n => Int.negOfNat n | Int.negSucc n => Int.ofNat (Nat.succ n)

source

def Int.subNatNat (m : Nat) (n : Nat) :

Int

Equations

Int.subNatNat m n = match n - m with | 0 => Int.ofNat (m - n) | Nat.succ k => Int.negSucc k

source

@[extern lean_int_add]

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

Int

Equations

Int.add m n = match m, n with | Int.ofNat m, Int.ofNat n => Int.ofNat (m + n) | Int.ofNat m, Int.negSucc n => Int.subNatNat m (Nat.succ n) | Int.negSucc m, Int.ofNat n => Int.subNatNat n (Nat.succ m) | Int.negSucc m, Int.negSucc n => Int.negSucc (Nat.succ (m + n))

source

@[extern lean_int_mul]

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

Int

Equations

Int.mul m n = match m, n with | Int.ofNat m, Int.ofNat n => Int.ofNat (m * n) | Int.ofNat m, Int.negSucc n => Int.negOfNat (m * Nat.succ n) | Int.negSucc m, Int.ofNat n => Int.negOfNat (Nat.succ m * n) | Int.negSucc m, Int.negSucc n => Int.ofNat (Nat.succ m * Nat.succ n)

source

@[defaultInstance 1000]

instance Int.instNegInt :

Neg Int

Equations

Int.instNegInt = { neg := Int.neg }

source

instance Int.instAddInt :

Add Int

Equations

Int.instAddInt = { add := Int.add }

source

instance Int.instMulInt :

Mul Int

Equations

Int.instMulInt = { mul := Int.mul }

source

@[extern lean_int_sub]

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

Int

Equations

Int.sub m n = m + -n

source

instance Int.instSubInt :

Sub Int

Equations

Int.instSubInt = { sub := Int.sub }

source

inductive Int.NonNeg :

Int → Prop

mk: ∀ (n : Nat), Int.NonNeg (Int.ofNat n)

source

noncomputable def Int.le (a : Int) (b : Int) :

Prop

Equations

Int.le a b = Int.NonNeg (b - a)

source

instance Int.instLEInt :

LE Int

Equations

Int.instLEInt = { le := Int.le }

source

noncomputable def Int.lt (a : Int) (b : Int) :

Prop

Equations

Int.lt a b = (a + 1 ≤ b)

source

instance Int.instLTInt :

LT Int

Equations

Int.instLTInt = { lt := Int.lt }

source

@[extern lean_int_dec_eq]

def Int.decEq (a : Int) (b : Int) :

Decidable (a = b)

Equations

Int.decEq a b = match a, b with | Int.ofNat a, Int.ofNat b => match decEq a b with | isTrue h => isTrue (_ : Int.ofNat a = Int.ofNat b) | isFalse h => isFalse (_ : Int.ofNat a = Int.ofNat b → False) | Int.negSucc a, Int.negSucc b => match decEq a b with | isTrue h => isTrue (_ : Int.negSucc a = Int.negSucc b) | isFalse h => isFalse (_ : Int.negSucc a = Int.negSucc b → False) | Int.ofNat a, Int.negSucc a_1 => isFalse (_ : Int.ofNat a = Int.negSucc a_1 → Int.noConfusionType False (Int.ofNat a) (Int.negSucc a_1)) | Int.negSucc a, Int.ofNat a_1 => isFalse (_ : Int.negSucc a = Int.ofNat a_1 → Int.noConfusionType False (Int.negSucc a) (Int.ofNat a_1))

source

instance Int.instDecidableEqInt :

DecidableEq Int

Equations

Int.instDecidableEqInt = Int.decEq

source

@[extern lean_int_dec_le]

instance Int.decLe (a : Int) (b : Int) :

Decidable (a ≤ b)

Equations

Int.decLe a b = Int.decNonneg (b - a)

source

@[extern lean_int_dec_lt]

instance Int.decLt (a : Int) (b : Int) :

Decidable (a < b)

Equations

Int.decLt a b = Int.decNonneg (b - (a + 1))

source

@[extern lean_nat_abs]

def Int.natAbs (m : Int) :

Nat

Equations

Int.natAbs m = match m with | Int.ofNat m => m | Int.negSucc m => Nat.succ m

source

instance Int.instOfNatInt {n : Nat} :

OfNat Int n

Equations

Int.instOfNatInt = { ofNat := Int.ofNat n }

source

@[extern lean_int_div]

def Int.div :

Int → Int → Int

Equations

Int.div _fun_discr _fun_discr = match _fun_discr, _fun_discr with | Int.ofNat m, Int.ofNat n => Int.ofNat (m / n) | Int.ofNat m, Int.negSucc n => -Int.ofNat (m / Nat.succ n) | Int.negSucc m, Int.ofNat n => -Int.ofNat (Nat.succ m / n) | Int.negSucc m, Int.negSucc n => Int.ofNat (Nat.succ m / Nat.succ n)

source

@[extern lean_int_mod]

def Int.mod :

Int → Int → Int

Equations

Int.mod _fun_discr _fun_discr = match _fun_discr, _fun_discr with | Int.ofNat m, Int.ofNat n => Int.ofNat (m % n) | Int.ofNat m, Int.negSucc n => Int.ofNat (m % Nat.succ n) | Int.negSucc m, Int.ofNat n => -Int.ofNat (Nat.succ m % n) | Int.negSucc m, Int.negSucc n => -Int.ofNat (Nat.succ m % Nat.succ n)

source

instance Int.instDivInt :

Div Int

Equations

Int.instDivInt = { div := Int.div }

source

instance Int.instModInt :

Mod Int

Equations

Int.instModInt = { mod := Int.mod }

source

def Int.toNat :

Int → Nat

Equations

Int.toNat _fun_discr = match _fun_discr with | Int.ofNat n => n | Int.negSucc a => 0

source

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

Nat

Equations

Int.natMod m n = Int.toNat (m % n)

source

def Int.pow (m : Int) :

Nat → Int

Equations

Int.pow m 0 = 1
Int.pow m (Nat.succ m_1) = Int.pow m m_1 * m

source

instance Int.instHPowIntNat :

HPow Int Nat Int

Equations

Int.instHPowIntNat = { hPow := Int.pow }

source

noncomputable instance Int.instLawfulBEqIntInstBEqInstDecidableEqInt :

LawfulBEq Int

Equations

Int.instLawfulBEqIntInstBEqInstDecidableEqInt = Int.instLawfulBEqIntInstBEqInstDecidableEqInt.proof_1