mathlib3 documentation

core / init.data.int.bitwise

def int.div2 :

Equations

-[1+ n].div2 = -[1+ n.div2 ]
(int.of_nat n).div2 = ↑(n.div2)

@[simp]

def int.bodd :

Equations

-[1+ n].bodd = !n.bodd
(int.of_nat n).bodd = n.bodd

def int.bit (b : bool) :

Equations

int.bit b = cond b bit1 bit0

def int.test_bit :

ℤ → ℕ → bool

Equations

-[1+ m].test_bit n = !m.test_bit n
↑m.test_bit n = m.test_bit n

def int.nat_bitwise (f : bool → bool → bool) (m n : ℕ) :

Equations

int.nat_bitwise f m n = cond (f bool.ff bool.ff) -[1+ nat.bitwise (λ (x y : bool), !f x y) m n] ↑(nat.bitwise f m n)

def int.bitwise (f : bool → bool → bool) :

ℤ → ℤ → ℤ

Equations

int.bitwise f -[1+ m] -[1+ n] = int.nat_bitwise (λ (x y : bool), f (!x) (!y)) m n
int.bitwise f -[1+ m] ↑n = int.nat_bitwise (λ (x y : bool), f (!x) y) m n
int.bitwise f ↑m -[1+ n] = int.nat_bitwise (λ (x y : bool), f x (!y)) m n
int.bitwise f ↑m ↑n = int.nat_bitwise f m n

def int.lnot :

Equations

-[1+ m].lnot = ↑m
↑m.lnot = -[1+ m]

def int.lor :

ℤ → ℤ → ℤ

Equations

def int.land :

ℤ → ℤ → ℤ

Equations

-[1+ m].land -[1+ n] = -[1+ m.lor n]
-[1+ m].land ↑n = ↑(n.ldiff m)
↑m.land -[1+ n] = ↑(m.ldiff n)
↑m.land ↑n = ↑(m.land n)

def int.ldiff :

ℤ → ℤ → ℤ

Equations

def int.lxor :

ℤ → ℤ → ℤ

Equations

-[1+ m].lxor -[1+ n] = ↑(m.lxor n)
-[1+ m].lxor ↑n = -[1+ m.lxor n]
↑m.lxor -[1+ n] = -[1+ m.lxor n]
↑m.lxor ↑n = ↑(m.lxor n)

def int.shiftl :

ℤ → ℤ → ℤ

Equations

-[1+ m].shiftl -[1+ n] = -[1+ m.shiftr n.succ]
-[1+ m].shiftl ↑n = -[1+ nat.shiftl' bool.tt m n]
↑m.shiftl -[1+ n] = ↑(m.shiftr n.succ)
↑m.shiftl ↑n = ↑(m.shiftl n)

def int.shiftr (m n : ℤ) :

Equations

m.shiftr n = m.shiftl (-n)