From 7eaf255d2f4c0c48d7832795e0ffd04f5f99407d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 4 Jul 2020 17:48:59 +0200
Subject: [PATCH] mention that the ASCII syntax exists (but we recommend
 unicode)

---
 docs/editor.md | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/docs/editor.md b/docs/editor.md
index 40edd49c0..df25c9393 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
-- 
GitLab