_CoqProject · c1a30c5800aba1f892bac7bad0faaea8609ba07b · Pierre Roux / Iris

Forked from Iris / Iris

Source project has a limited visibility.

5 years ago

ascii notation for most iris operators. · c1a30c58

Gregory Malecha authored 5 years ago

- all ascii notation is marked "only parsing" so this PR shouldn't
  change anything for anyone using only unicode notation.
- the algorithm for creating an ascii notation is pretty simple.
  - \ast -> *
  - \triangleright -> |>
  - \vee -> \/
  - \wedge -> /\
  - \forall -> forall
  - \exists -> exists
  - \ast -> **

c1a30c58

History

ascii notation for most iris operators.

Gregory Malecha authored 5 years ago

- all ascii notation is marked "only parsing" so this PR shouldn't
  change anything for anyone using only unicode notation.
- the algorithm for creating an ascii notation is pretty simple.
  - \ast -> *
  - \triangleright -> |>
  - \vee -> \/
  - \wedge -> /\
  - \forall -> forall
  - \exists -> exists
  - \ast -> **