Init.Data.Nat.Bitwise

source

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

Nat

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 x 0 = x
Nat.shiftLeft x (Nat.succ m) = Nat.shiftLeft (2 * x) m

source

@[extern lean_nat_shiftr]

def Nat.shiftRight :

Nat → Nat → Nat

Equations

Nat.shiftRight x 0 = x
Nat.shiftRight x (Nat.succ m) = Nat.shiftRight x 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 }