Port some docs by Ed Ayers's edlib repo

[bryangingechen]

@EdAyers wrote some nice explanations of various aspects of Lean 3 in his "edlib" repo, including e.g. an explanation of unicode in Lean and a series of articles on meta code.

On Zulip he gave his permission for us to do what we like with them.