All names in Lean (names of symbols and modules) are stored as their raw form (list[int | str]) instead of the usual pretty-printed form to avoid problems arising from quoting/unquoting.
For example, instead of "Lean.«binderTerm∉»" we have ["Lean", "binderTerm∉"].
