@@ -366,6 +366,25 @@ public partial
366366sext : Bits n -> Bits (n+m)
367367sext (MkBits x) = MkBits (sext' x)
368368
369+-- TODO: Prove
370+%assert_total
371+trunc' : machineTy (log2Bytes (n+m)) -> machineTy (log2Bytes n)
372+trunc' {n=n} {m=m} x with (log2Bytes n, log2Bytes (n+m))
373+ | (O, O) = believe_me x
374+ | (O, S O) = believe_me (prim__truncB16_8 (believe_me x))
375+ | (O, S (S O)) = believe_me (prim__truncB32_8 (believe_me x))
376+ | (O, S (S (S _))) = believe_me (prim__truncB64_8 (believe_me x))
377+ | (S O, S O) = believe_me x
378+ | (S O, S (S O)) = believe_me (prim__truncB32_16 (believe_me x))
379+ | (S O, S (S (S _))) = believe_me (prim__truncB64_16 (believe_me x))
380+ | (S (S O), S (S O)) = believe_me x
381+ | (S (S O), S (S (S _))) = believe_me (prim__truncB64_32 (believe_me x))
382+ | (S (S (S _)), S (S (S _))) = believe_me x
383+
384+public partial
385+truncate : Bits (n+m) -> Bits n
386+truncate (MkBits x) = MkBits (trunc' x)
387+
369388public
370389bitSet : Fin n -> Bits n -> Bool
371390bitSet n x = bitsAnd (intToBits 1 `bitsShl` intToBits (cast (finToNat n))) x /= intToBits 0