Documentation

Init.Data.Nat.Bitwise

theorem Nat.bitwise_rec_lemma {n : Nat} (hNe : n ≠ 0) :

n / 2 < n

def Nat.bitwise (f : Bool → Bool → Bool) (n : Nat) (m : Nat) :

Equations

Nat.bitwise f n m = if n = 0 then if f false true = true then m else 0 else if m = 0 then if f true false = true then n else 0 else let n' := n / 2; let m' := m / 2; let b₁ := n % 2 = 1; let b₂ := m % 2 = 1; let r := Nat.bitwise f n' m'; if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r

@[extern lean_nat_land]

def Nat.land :

Nat → Nat → Nat

Equations

Nat.land = Nat.bitwise and

@[extern lean_nat_lor]

def Nat.lor :

Nat → Nat → Nat

Equations

Nat.lor = Nat.bitwise or

@[extern lean_nat_lxor]

def Nat.xor :

Nat → Nat → Nat

Equations

Nat.xor = Nat.bitwise bne

@[extern lean_nat_shiftl]

def Nat.shiftLeft :

Nat → Nat → Nat

Equations

Nat.shiftLeft _fun_discr 0 = _fun_discr
Nat.shiftLeft _fun_discr (Nat.succ m) = Nat.shiftLeft (2 * _fun_discr) m

@[extern lean_nat_shiftr]

def Nat.shiftRight :

Nat → Nat → Nat

Equations

Nat.shiftRight _fun_discr 0 = _fun_discr
Nat.shiftRight _fun_discr (Nat.succ m) = Nat.shiftRight _fun_discr m / 2

instance Nat.instAndOpNat :

Equations

Nat.instAndOpNat = { and := Nat.land }

instance Nat.instOrOpNat :

Equations

Nat.instOrOpNat = { or := Nat.lor }

instance Nat.instXorNat :

Equations

Nat.instXorNat = { xor := Nat.xor }

instance Nat.instShiftLeftNat :

Equations

Nat.instShiftLeftNat = { shiftLeft := Nat.shiftLeft }

instance Nat.instShiftRightNat :

Equations

Nat.instShiftRightNat = { shiftRight := Nat.shiftRight }