• 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.
    295cacf4
Name
Last commit
Last update
..
glob.ml Loading commit data...
glob.mli Loading commit data...
handcrafted.messages Loading commit data...
lexer.mli Loading commit data...
lexer.mll Loading commit data...
parser.mly Loading commit data...
ptree.ml Loading commit data...
report.ml Loading commit data...
report.mli Loading commit data...
typing.ml Loading commit data...
typing.mli Loading commit data...