bit operations

def Int.not : Int → Int

Bitwise not, usually accessed via the ~~~ prefix operator.

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

Examples:

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

Equations

• (Int.ofNat n).not = Int.negSucc n
• (Int.negSucc n).not = Int.ofNat n

instance Int.instComplement : Complement Int

Equations

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

def Int.shiftRight : Int → Nat → Int

Bitwise right shift, usually accessed via the >>> operator.

Interprets the integer as an infinite sequence of bits in two's complement and shifts the value to the right.

Examples:

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

Equations

• (Int.ofNat n).shiftRight x✝ = Int.ofNat (n >>> x✝)
• (Int.negSucc n).shiftRight x✝ = Int.negSucc (n >>> x✝)

instance Int.instHShiftRightNat : HShiftRight Int Nat Int

Equations

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

def Int.shiftLeft : Int → Nat → Int

Bitwise left shift, usually accessed via the <<< operator.

Examples:

• 1 <<< 2 = 4
• 1 <<< 3 = 8
• 0 <<< 3 = 0
• 0xf1 <<< 4 = 0xf10
• (-1) <<< 3 = -8

Equations

• (Int.ofNat n).shiftLeft x✝ = Int.ofNat (n <<< x✝)
• (Int.negSucc n).shiftLeft x✝ = Int.negSucc ((n + 1) <<< x✝ - 1)

instance Int.instHShiftLeftNat : HShiftLeft Int Nat Int

Equations

• Int.instHShiftLeftNat = { hShiftLeft := Int.shiftLeft }