@@ -328,6 +328,25 @@ public
328328complement : Bits n -> Bits n
329329complement (MkBits x) = MkBits (complement' x)
330330
331+-- TODO: Prove
332+%assert_total
333+zext' : machineTy (log2Bytes n) -> machineTy (log2Bytes (n+m))
334+zext' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
335+ | (O, O) = believe_me x
336+ | (O, S O) = believe_me (prim__zextB8_16 (believe_me x))
337+ | (O, S (S O)) = believe_me (prim__zextB8_32 (believe_me x))
338+ | (O, S (S (S _))) = believe_me (prim__zextB8_64 (believe_me x))
339+ | (S O, S O) = believe_me x
340+ | (S O, S (S O)) = believe_me (prim__zextB16_32 (believe_me x))
341+ | (S O, S (S (S _))) = believe_me (prim__zextB16_64 (believe_me x))
342+ | (S (S O), S (S O)) = believe_me x
343+ | (S (S O), S (S (S _))) = believe_me (prim__zextB32_64 (believe_me x))
344+ | (S (S (S _)), S (S (S _))) = believe_me x
345+
346+public partial
347+zext : Bits n -> Bits (n+m)
348+zext (MkBits x) = MkBits (zext' x)
349+
331350public
332351bitSet : Fin n -> Bits n -> Bool
333352bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0