mention that the ASCII syntax exists (but we recommend unicode)

docs/editor.md

 Here we collect some information on how to set up your editor to properly input
 and output the unicode characters used throughout Iris.
 
+If you really want to, you can also avoid having to type unicode characters by
+importing `iris.bi.ascii`.  That enables parsing-only ASCII alternatives to many
+unicode notations. (Feel free to report an issue when you notice that a notation
+is missing.)  The easiest way to learn the ASCII syntax is to
+[read this file](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/bi/ascii.v).
+Note however that this will make your code harder to read and work on for Iris
+developers that are used to our default unicode notation---generally, our
+recommendation is to use the unicode syntax whenever possible.
+
 ## General: Unicode Fonts
 
 Most editors will just use system fonts for rendering unicode characters and do