@@ -317,6 +317,17 @@ instance Ord (Bits n) where
320+complement' : machineTy n -> machineTy n
321+complement' {n=n} x with n
322+ | O = prim__complB8 x
323+ | S O = prim__complB16 x
324+ | S (S O) = prim__complB32 x
325+ | S (S (S _)) = prim__complB64 x
328+complement : Bits n -> Bits n
329+complement (MkBits x) = MkBits (complement' x)
321bitSet : Fin n -> Bits n -> Bool
332bitSet : Fin n -> Bits n -> Bool
322bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0
333bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0