Add support for builtin Byte (#118)

> ⚠️ Depends on:
> * #117
> * anoma/juvix#2918

Adds support for the builtin Byte type introduced in:
* anoma/juvix#2918

Stdlib/Data/Byte.juvix

@@ -0,0 +1,28 @@
+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.String.Base open;
+
+import Stdlib.Trait.Eq open public;
+import Stdlib.Trait.FromNatural open;
+import Stdlib.Trait.Show open public;
+
+{-# specialize: true, inline: case #-}
+instance
+eqByteI : Eq Byte := mkEq (Byte.==);
+
+instance
+showByteI : Show Byte :=
+  mkShow@{
+    show := Byte.toNat >> Show.show
+  };
+
+{-# specialize: true, inline: case #-}
+instance
+fromNaturalByteI : FromNatural Byte :=
+  mkFromNatural@{
+    fromNat := Byte.fromNat
+  };

Stdlib/Data/Byte/Base.juvix

@@ -0,0 +1,22 @@
+module Stdlib.Data.Byte.Base;
+
+import Stdlib.Data.Bool.Base open;
+import Stdlib.Data.Fixity open;
+import Stdlib.Data.Nat.Base open;
+
+--- An 8-bit unsigned integer.
+builtin byte
+axiom Byte : Type;
+
+--- Converts a ;Nat; to a ;Byte;. It takes the modulus of the input natural number with 256.
+builtin byte-from-nat
+axiom fromNat : Nat -> Byte;
+
+--- Converts a ;Byte; to the corresponding ;Nat;.
+builtin byte-to-nat
+axiom toNat : Byte -> Nat;
+
+syntax operator == comparison;
+
+builtin byte-eq
+axiom == : Byte -> Byte -> Bool;

Stdlib/Prelude.juvix

@@ -4,6 +4,7 @@ module Stdlib.Prelude;
 import Stdlib.Data.Fixity open public;
 
 import Stdlib.Data.Bool open public;
+import Stdlib.Data.Byte open public;
 import Stdlib.Data.Unit open public;
 import Stdlib.Data.List open public;
 import Stdlib.Data.Maybe open public;