Problem 13

(Intermediate 🌟🌟) Implement the so-called run-length encoding data compression method directly. I.e. don't explicitly create the sublists containing the duplicates, as in Problem 9, but only count them. As in Problem 11, simplify the result list by replacing the singleton lists (1 X) by X.

variable {α : Type} [BEq α] [Inhabited α]

inductive Data (α : Type) where
  | multiple : Nat → α → Data α
  | single : α → Data α
deriving Repr

open Data

def encodeDirect (l : List α) : List (Data α) :=
  sorry

-- The following codes are for test and you should not edit these.

example : encodeDirect ['a', 'a', 'b', 'c'] =
  [multiple 2 'a', single 'b', single 'c'] := by rfl

example : encodeDirect ([] : List α) = [] := by rfl

example : encodeDirect ['a', 'b', 'b', 'b', 'c', 'b', 'b'] =
  [single 'a', multiple 3 'b', single 'c', multiple 2 'b'] := by rfl