Pretty printing custom list literal

Stream: lean4

[ohhaimark]

What is actually used to pretty print List in lean? I have a list literal notation for Vec, implemented Repr, ToFormat and looked at the Delaborator for reference, but I can't figure it out.

[Mac]

These @[appUnexpander] definitions from Init.NotationExtra:

@[appUnexpander List.nil] def unexpandListNil : Lean.PrettyPrinter.Unexpander
  | `($(_)) => `([])
  | _       => throw ()

@[appUnexpander List.cons] def unexpandListCons : Lean.PrettyPrinter.Unexpander
  | `($(_) $x [])      => `([$x])
  | `($(_) $x [$xs,*]) => `([$x, $xs,*])
  | _                  => throw ()

See the source code here.