Port some docs by Ed Ayers's edlib repo #153
Description
@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.