Init.Data.Nat.Bitwise

source

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

n / 2 < n

source

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

Nat

Equations

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

source

@[extern lean_nat_land]

def Nat.land:

Nat → Nat → Nat

Equations

Nat.land = Nat.bitwise and

source

@[extern lean_nat_lor]

def Nat.lor:

Nat → Nat → Nat

Equations

Nat.lor = Nat.bitwise or

source

@[extern lean_nat_lxor]

def Nat.xor:

Nat → Nat → Nat

Equations

Nat.xor = Nat.bitwise bne

source

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

source

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

source

instance Nat.instAndOpNat:

AndOp Nat

Equations

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

source

instance Nat.instOrOpNat:

OrOp Nat

Equations

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

source

instance Nat.instXorNat:

Xor Nat

Equations

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

source

instance Nat.instShiftLeftNat:

ShiftLeft Nat

Equations

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

source

instance Nat.instShiftRightNat:

ShiftRight Nat

Equations

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