def Auto.Int.beq : Int → Int → Bool

Equations

• Auto.Int.beq (Int.ofNat n₁) (Int.ofNat n₂) = n₁.beq n₂
• Auto.Int.beq (Int.negSucc n₁) (Int.negSucc n₂) = n₁.beq n₂
• Auto.Int.beq x✝¹ x✝ = false

instance Auto.instBEqInt_auto : BEq Int

Equations

• Auto.instBEqInt_auto = { beq := Auto.Int.beq }

theorem Auto.Int.beq_def {a b : Int} : (a == b) = beq a b

def Auto.Int.beq_refl {i : Int} : beq i i = true

Equations

• ⋯ = ⋯

def Auto.Int.eq_of_beq_eq_true {i₁ i₂ : Int} : beq i₁ i₂ = true → i₁ = i₂

Equations

• ⋯ = ⋯

instance Auto.instLawfulBEqInt_auto : LawfulBEq Int

def Auto.Int.abs (x : Int) : Int

Equations

• Auto.Int.abs x = if x ≤ -x then -x else x

theorem Auto.Int.shiftRight_def (i : Int) (s : Nat) : i >>> s = match i with | Int.ofNat n => Int.ofNat (n >>> s) | Int.negSucc n => Int.negSucc (n >>> s)