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

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

source

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

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

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

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

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

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

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

source

@[extern lean_int_mod]

def Int.mod:

Int → Int → Int

Equations

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

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

instance Int.instLawfulBEqIntInstBEqInstDecidableEqInt:

LawfulBEq Int

Equations

Int.instLawfulBEqIntInstBEqInstDecidableEqInt = Int.instLawfulBEqIntInstBEqInstDecidableEqInt.proof_1