1) I'm often copy/pasting from publications, and the PDF-rendered glyphs don't turn into proper unicode either (OSX, Preview, paste to Firefox, at least)
2) There are conventional differences between the different arrows such as using a arrow with or without a superscript star versus single-bar down versus double-bar down, etc. and trying to render those in ASCII would be quite confusing for the reader and author. Each of them have semantic meanings, and putting in what is usually used as a single-step arrow in a big-step semantics because you lack the glyphs makes an experienced reader's head hurt.
1) I'm often copy/pasting from publications, and the PDF-rendered glyphs don't turn into proper unicode either (OSX, Preview, paste to Firefox, at least)
2) There are conventional differences between the different arrows such as using a arrow with or without a superscript star versus single-bar down versus double-bar down, etc. and trying to render those in ASCII would be quite confusing for the reader and author. Each of them have semantic meanings, and putting in what is usually used as a single-step arrow in a big-step semantics because you lack the glyphs makes an experienced reader's head hurt.