Resolved

Stream: general

[Erika Su]

Just to be sure: lean currently doesn't support nested pattern matching, right? Because such code cannot compile.

def toFmt(l: List (Nat ⊕ String)): Fmt :=
  match l with
    | nil => Fmt.nil
    | cons (inl n) tail => Fmt.str <| toFmt tail
    | cons (inr str) tail => Fmt.num <| toFmt tail
  ```

[Notification Bot]

Erika Su has marked this topic as resolved.

[Notification Bot]

Erika Su has marked this topic as unresolved.