• Andrei Paskevich's avatar
    Ident: disambiguated symbolic notation · 295cacf4
    Andrei Paskevich authored
    It is possible to append an arbitary number of quote symbols
    at the end of an prefix/infix/mixfix operator:
                applied form      standalone form
                  -' 42               (-'_)
                  x +' y              (+')
                  a[0]' <- 1          ([]'<-)
    Pretty-printing will use the quote symbols for disambiguation.
    The derived symbols can be produced by Why3 by appending
    a suffix of the form "_toto" or "'toto". These symbols can
    be parsed/printed as "(+)_toto" or "(+)'toto", respectively.
driver_lexer.mll 3.88 KB