Add stupid decoder too

Changes

1 changed files (+15/-2)

• Puzzle.lean
  • @@ -1,9 +1,22 @@
    - def s := "hello world" + def s := "hi" - #eval s.toList.map (λ x ↦ + 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 (λ y ↦ y == " ") + |>.foldl (λ acc x ↦ + if acc.2.length = 7 then + (acc.1 ++ (acc.2 ++ [x] + |> BitVec.ofBoolListBE + |>.toNat + |> Char.ofNat).toString, []) + else (acc.1, acc.2 ++ [x])) ("", []) + |>.1 + + #eval encode s |> decode