1	import Base
2	
3	type Bytes.Error is Data:
4	  InvalidByte{index: Nat, value: U32}
5	
6	type Bytes is Data:
7	  Bytes{data: List<&2, U32>}
8	
9	def Bytes.ok_byte(x: U32) -> Bool:
10	  U32.is_le(x, 255)
11	
12	def Bytes.from_u32_list.go(
13	  xs: List<&2, U32>, acc: List<&2, U32>, i: Nat, ok: Bool, +h: U32
14	) -> Result<&2, &2, Bytes.Error, Bytes>:
15	  match xs ok:
16	    case _ False{}:
17	      Fail{InvalidByte{i, h}}
18	    case Nil{} True{}:
19	      Done{Bytes{List.reverse(&2, U32, Con{h, acc})}}
20	    case Con{+hh, t} True{}:
21	      Bytes.from_u32_list.go(t, Con{h, acc}, 1n+i, Bytes.ok_byte(hh), hh)
22	
23	def Bytes.from_u32_list.start(
24	  xs: List<&2, U32>
25	) -> Result<&2, &2, Bytes.Error, Bytes>:
26	  match xs:
27	    case Nil{}:
28	      Done{Bytes{Nil{}}}
29	    case Con{+h, t}:
30	      Bytes.from_u32_list.go(t, Nil{}, 0n, Bytes.ok_byte(h), h)
31	
32	def Bytes.from_u32_list(
33	  values: List<&2, U32>
34	) -> Result<&2, &2, Bytes.Error, Bytes>:
35	  Bytes.from_u32_list.start(values)
36	
37	def Bytes.to_u32_list(b: Bytes) -> List<&2, U32>:
38	  match b:
39	    case Bytes{data}:
40	      data