@@ -501,5 +501,13 @@ bitsToStr x = pack (helper last x)
501501 helper FZ _ = []
502502 helper (FS x) b = assert_total $ (if getBit x b then '1' else '0') :: helper (weaken x) b
503503
504+bitsToHexStr : %static {n : Nat} -> Bits n -> String
505+bitsToHexStr {n} (MkBits b) with (nextBytes n)
506+ | Z = b8ToHexString b
507+ | S Z = b16ToHexString b
508+ | S (S Z) = b32ToHexString b
509+ | S (S (S Z)) = b64ToHexString b
510+ | _ = assert_unreachable
511+
504512implementation Show (Bits n) where
505513 show = bitsToStr