bit operations

def Int.not : Int → Int

Bitwise not

Interprets the integer as an infinite sequence of bits in two's complement and complements each bit.

~~~(0:Int) = -1
~~~(1:Int) = -2
~~~(-1:Int) = 0

Equations

• x.not = match x with | Int.ofNat n => Int.negSucc n | Int.negSucc n => Int.ofNat n

instance Int.instComplement : Complement Int

Equations

• Int.instComplement = { complement := Int.not }

def Int.shiftRight : Int → Nat → Int

Bitwise shift right.

Conceptually, this treats the integer as an infinite sequence of bits in two's complement and shifts the value to the right.

( 0b0111:Int) >>> 1 =  0b0011
( 0b1000:Int) >>> 1 =  0b0100
(-0b1000:Int) >>> 1 = -0b0100
(-0b0111:Int) >>> 1 = -0b0100

Equations

• x✝.shiftRight x = match x✝, x with | Int.ofNat n, s => Int.ofNat (n >>> s) | Int.negSucc n, s => Int.negSucc (n >>> s)

instance Int.instHShiftRightNat : HShiftRight Int Nat Int

Equations

• Int.instHShiftRightNat = { hShiftRight := Int.shiftRight }