ascii notation for most iris operators.
- 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 -> **
Showing
- CHANGELOG.md 20 additions, 1 deletionCHANGELOG.md
- _CoqProject 1 addition, 0 deletions_CoqProject
- tests/proofmode_ascii.ref 150 additions, 0 deletionstests/proofmode_ascii.ref
- tests/proofmode_ascii.v 260 additions, 0 deletionstests/proofmode_ascii.v
- theories/bi/ascii.v 81 additions, 0 deletionstheories/bi/ascii.v
Loading
Please register or sign in to comment