Mentions légales du service

Skip to content
  • 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