diff --git a/docs/editor.md b/docs/editor.md
index 40edd49c0ab1ea3798c4ecf4c4aa56999e3da4e3..df25c939357c1f53a1520834a450a7db2b735a8e 100644
--- a/docs/editor.md
+++ b/docs/editor.md
@@ -1,6 +1,15 @@
 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