Skip to content

Fix notation issues in #302 and add some missing "operator sections" for (bi)entailment

Paolo G. Giarrusso requested to merge Blaisorblade/iris:fix-notation-3 into master

Fix #302 (closed) (and its new instance in !396 (merged)):

  • Add missing spaces when declaring notations. This enables spaces within certain sections, as requested, but that is inconsistent with other notations, so should be reconsidered — see my review comment below.
  • That leaves an ambiguity for ⊢@{; fix that by adding a notation ( '⊢@{' PROP } Q ) to enable left-factoring (see source-code comment for details).

Also, add new notations (.⊢ Q), (P ⊢.), (P ⊣⊢.), (.⊣⊢ Q), as requested by @robbertkrebbers, and their ASCII variants for consistency. Finally, add a bunch of new testcases with different combinations of spaces as requested.

Edited by Paolo G. Giarrusso

Merge request reports