Skip to content
  • Paolo G. Giarrusso's avatar
    Fix entailment notations `(⊢@{PROP})` and `(⊣⊢@{PROP} )` etc. · 1b820fbf
    Paolo G. Giarrusso authored
    Fix #302, including their ASCII variants.
    - Don't use quotes `'` that are not surrounded by spaces.
    - However, notation `'(⊢@{' PROP } )` prevents parsing `(⊢@{PROP} Q)` using the
    `⊢@{PROP} Q` notation.
    
    To fix that, we force left-factorization: we add a notation for `'(⊢@{' PROP }
    Q )`, defined to coincide with '⊢@{' PROP } Q but which can be left-factored
    with `( '⊢@{' PROP } )`.
    
    - Add left and right operator sections for (bi)entailment
    - Add tests.
    
    Also do all of the above also for ASCII notations, except for operator sections,
    which seem to require more discussion.
    1b820fbf