Problem 7

(Intermediate 🌟🌟) Flatten a nested list structure.

variable {α : Type}

-- We have to define a new data type, because lists in Lean are homogeneous.
inductive NestedList (α : Type) where
  | elem : α → NestedList α
  | list : List (NestedList α) → NestedList α

section
  /-!
  ## Pretty printing of NestedList
  Display `NestedList` in a readable manner when you run `#eval`.
  When solving this problem, **do not mind** the contents of this section.

  The following code was provided by Mario Carneiro.
  -/
  open Std in

  partial def NestedList.repr [Repr α] (a : NestedList α) (n : Nat) : Format :=
    let _ : ToFormat (NestedList α) := ⟨(NestedList.repr · 0)⟩
    match a, n with
    | elem x, _ => reprPrec x n
    | list as, _ => Format.bracket "[" (Format.joinSep as ("," ++ Format.line)) "]"

  instance [Repr α] : Repr (NestedList α) where
    reprPrec := NestedList.repr
end

/-- flatten the list structure -/
def flatten (nl : NestedList α) : List α :=
  sorry

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

open NestedList

def sample : NestedList Nat :=
  list [elem 1, list [elem 2, elem 3], elem 4]

#eval sample

def empty : NestedList String := list []

#eval empty

example : flatten (elem 5) = [5] := rfl

example : flatten sample = [1, 2, 3, 4] := rfl

example : flatten (empty) = [] := rfl