• Andrei Paskevich's avatar
    WhyML: change the syntax of "abstract" · 4fd8b24d
    Andrei Paskevich authored
    The old syntax:   abstract expr [spec]...
    
    The semicolon binds more loosely than "abstract" and
    the specification clauses are optional, so that
    "abstract e1; e2" is the same as "(abstract e1); e2"
    and "abstract e1; e2; ensures {...}" is a syntax error.
    
    The new syntax:   abstract [spec]... expr end
    
    This allows to put sequences of expressions under "abstract"
    without ambiguity and moves the specification clauses to the
    beginning. In other words, "abstract" becomes a "begin" with
    a specification attached. The spec-at-the-top is consistent
    with the syntax of functions and the whole seems to be more
    natural for the intented use of "abstract" (a logical cut).
    4fd8b24d
Name
Last commit
Last update
..
bash Loading commit data...
emacs Loading commit data...
images Loading commit data...
javascript Loading commit data...
lang Loading commit data...
latex Loading commit data...
vim Loading commit data...
zsh Loading commit data...
drivers Loading commit data...
modules Loading commit data...
provers-detection-data.conf Loading commit data...
theories Loading commit data...
why3session.dtd Loading commit data...