@@ -317,6 +317,17 @@ instance Ord (Bits n) where
317317 then EQ
318318 else GT
319319
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
326+
327+public
328+complement : Bits n -> Bits n
329+complement (MkBits x) = MkBits (complement' x)
330+
320331public
321332bitSet : Fin n -> Bits n -> Bool
322333bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0