Equations
- Int.instInhabitedInt = { default := Int.ofNat 0 }
Equations
- Int.negOfNat x = match x with | 0 => 0 | Nat.succ m => Int.negSucc m
Equations
- Int.subNatNat m n = match n - m with | 0 => Int.ofNat (m - n) | Nat.succ k => Int.negSucc k
@[extern lean_int_add]
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))
@[extern lean_int_mul]
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)
@[defaultInstance 1000]
Equations
- Int.instNegInt = { neg := Int.neg }
@[extern lean_int_dec_eq]
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 b => isFalse (_ : Int.ofNat a = Int.negSucc b → Int.noConfusionType False (Int.ofNat a) (Int.negSucc b)) | Int.negSucc a, Int.ofNat b => isFalse (_ : Int.negSucc a = Int.ofNat b → Int.noConfusionType False (Int.negSucc a) (Int.ofNat b))
Equations
@[extern lean_nat_abs]
Equations
- Int.natAbs m = match m with | Int.ofNat m => m | Int.negSucc m => Nat.succ m
@[extern lean_int_div]
@[extern lean_int_mod]
Equations
- Int.instHPowIntNat = { hPow := Int.pow }