@@ -501,5 +501,13 @@ bitsToStr x = pack (helper last x)
501 helper FZ _ = []
501 helper FZ _ = []
502 helper (FS x) b = assert_total $ (if getBit x b then '1' else '0') :: helper (weaken x) b
502 helper (FS x) b = assert_total $ (if getBit x b then '1' else '0') :: helper (weaken x) b
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
504implementation Show (Bits n) where
512implementation Show (Bits n) where
505 show = bitsToStr
513 show = bitsToStr