Mentions légales du service

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