@@ -356,8 +356,8 @@ bitsToInt : Bits n -> Integer
356356bitsToInt (MkBits x) = bitsToInt' x
357357
358358-- Zero out the high bits of a truncated bitstring
359−--zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
360−--zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
359+zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)
360+zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)
361361
362362--instance Cast Nat (Bits n) where
363363-- cast x = MkBits (zeroUnused (natToBits n))
@@ -399,8 +399,8 @@ sext' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
399399
400400-- TODO: Prove
401401%assert_total -- can't verify coverage of with block
402−trunc' : machineTy (nextBytes (n+m)) -> machineTy (nextBytes n)
403−trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
402+trunc' : machineTy (nextBytes (m+n)) -> machineTy (nextBytes n)
403+trunc' {m=m} {n=n} x with (nextBytes n, nextBytes (m+n))
404404 | (Z, Z) = believe_me x
405405 | (Z, S Z) = believe_me (prim__truncB16_B8 (believe_me x))
406406 | (Z, S (S Z)) = believe_me (prim__truncB32_B8 (believe_me x))
@@ -412,9 +412,9 @@ trunc' {n=n} {m=m} x with (nextBytes n, nextBytes (n+m))
412412 | (S (S Z), S (S (S _))) = believe_me (prim__truncB64_B32 (believe_me x))
413413 | (S (S (S _)), S (S (S _))) = believe_me x
414414
415−--public
416−--truncate : Bits (n+m) -> Bits n
417−--truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
415+public
416+truncate : Bits (m+n) -> Bits n
417+truncate (MkBits x) = MkBits (zeroUnused (trunc' x))
418418
419419public
420420bitAt : Fin n -> Bits n