• Andrei Paskevich's avatar
    WhyML: allow return types with names: f (a:int) : (x: int, ghost y: int) · 0ffeb3d4
    Andrei Paskevich authored
    These names are only visible under "ensures" but not under "returns".
    If the result is named, the special variable "result" is not used.
    In a tuple, either each component should be named, or none at all.
    Underscores are allowed. Parentheses around the return type are required.
    Each name must be given its own type: "f () : (x y: int)" is rejected.
    Identifiers without cast are treated as types, not as names.
    To name the result without giving its type, use "returns".
    0ffeb3d4
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...