Commit 608ed52a authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ralf/ascii' into 'master'

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

See merge request !470
parents 6b0e19f5 04d223b9
Pipeline #31463 canceled with stage
in 12 minutes and 18 seconds
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. In particular,
Unicode syntax is required for MRs to Iris itself and other Iris-managed
repositories.
## General: Unicode Fonts
Most editors will just use system fonts for rendering unicode characters and do
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment