1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22

def s := "hi"

def encode (s : String) := s.toList.map (λ x ↦
  let bx := x.toUInt8.toBitVec
  List.range 8
    |>.map λ y ↦
      if bx.getMsbD y then " " else "")
  |>.flatten
  |> "f".intercalate

def decode (s : String) := s.splitOn "f"
  |>.map (· == " ")
  |>.foldl (λ (a, b) x ↦
    if b.length = 7 then
      (a ++ (b ++ [x]
        |> BitVec.ofBoolListBE
        |>.toNat
        |> Char.ofNat).toString, [])
    else (a, b ++ [x])) ("", [])
  |>.1

#eval encode s |> decode