Show Bytes in hexadecimal

Stdlib/Data/Byte.juvix

@@ -3,8 +3,9 @@ module Stdlib.Data.Byte;
 import Stdlib.Data.Byte.Base open using {Byte} public;
 import Stdlib.Data.Byte.Base as Byte public;
 import Stdlib.Function open;
-import Stdlib.Data.Nat;
+import Stdlib.Data.Nat open;
 import Stdlib.Data.String.Base open;
+import Stdlib.Debug.Fail open;
 
 import Stdlib.Trait.Eq open public;
 import Stdlib.Trait.FromNatural open;
@@ -17,7 +18,20 @@ eqByteI : Eq Byte := Eq.mk (Byte.==);
 instance
 showByteI : Show Byte :=
   Show.mk@{
-    show (x : Byte) : String := Show.show (Byte.toNat x);
+    show (x : Byte) : String :=
+      let
+        nibble (n : Nat) : String :=
+          if
+            | n <= 9 := Show.show n
+            | n == 10 := "A"
+            | n == 11 := "B"
+            | n == 12 := "C"
+            | n == 13 := "D"
+            | n == 14 := "E"
+            | n == 15 := "F"
+            | else := impossible;
+        nat := Byte.toNat x;
+      in "0x" ++str nibble (div nat 16) ++str nibble (mod nat 16);
   };
 
 {-# specialize: true, inline: case #-}

Stdlib/Debug/Fail.juvix

@@ -5,3 +5,5 @@ import Stdlib.Data.String.Base open;
 --- Exit the program with an error message.
 builtin fail
 axiom failwith : {A : Type} -> (message : String) -> A;
+
+impossible {A} : A := failwith "impossible";

Stdlib/Trait/Show.juvix

@@ -7,3 +7,5 @@ type Show A :=
   mk@{
     show : A -> String;
   };
+
+open Show using {show} public;

test/Package.juvix

@@ -12,6 +12,6 @@ package : Package :=
           "anoma"
           "juvix-quickcheck"
           "a78bf8da2e14f639f57e2f5e73f6a82fd3a8ff86";
-        github "anoma" "juvix-test" "d093e3dcc3caaea48433059810b671e38cfb02f7";
+        github "anoma" "juvix-test" "81a1ee5176055c1002eca0b5f9dcba665986f3ec";
       ];
   };