the Type, coercions, and notation

inductive Int : Type

• ofNat: Nat → Int
• negSucc: Nat → Int

instance instCoeNatInt : Coe Nat Int

Equations

• instCoeNatInt = { coe := Int.ofNat }

instance instOfNatInt {n : Nat} : OfNat Int n

Equations

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

instance Int.instInhabitedInt : Inhabited Int

Equations

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

def Int.negOfNat : Nat → Int

Equations

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

@[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)

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

@[extern lean_int_add]

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

Equations

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

@[extern lean_int_mul]

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

Equations

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

@[defaultInstance 500]

instance Int.instNegInt : Neg Int

The Neg Int default instance must have priority higher than low since the default instance OfNat Nat n has low priority.

#check -42

Equations

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

instance Int.instAddInt : Add Int

Equations

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

instance Int.instMulInt : Mul Int

Equations

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

@[extern lean_int_sub]

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

Equations

• Int.sub m n = m + -n

instance Int.instSubInt : Sub Int

Equations

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

inductive Int.NonNeg : Int → Prop

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

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

Equations

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

instance Int.instLEInt : LE Int

Equations

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

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

Equations

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

instance Int.instLTInt : LT Int

Equations

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

@[extern lean_int_dec_eq]

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

Equations

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

instance Int.instDecidableEqInt : DecidableEq Int

Equations

• Int.instDecidableEqInt = Int.decEq

@[extern lean_int_dec_le]

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

Equations

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

@[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))

@[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

@[extern lean_int_div]

def Int.div : Int → Int → Int

Equations

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

@[extern lean_int_mod]

def Int.mod : Int → Int → Int

Equations

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

instance Int.instDivInt : Div Int

Equations

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

instance Int.instModInt : Mod Int

Equations

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

def Int.toNat : Int → Nat

Equations

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

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

instance Int.instHPowIntNat : HPow Int Nat Int

Equations

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

instance Int.instLawfulBEqIntInstBEqInstDecidableEqInt : LawfulBEq Int

Equations

• Int.instLawfulBEqIntInstBEqInstDecidableEqInt = Int.instLawfulBEqIntInstBEqInstDecidableEqInt.proof_1

instance Int.instMinInt : Min Int

Equations

• Int.instMinInt = minOfLe

instance Int.instMaxInt : Max Int

Equations

• Int.instMaxInt = maxOfLe