GitLab

Also, ghost fields in algerbraic types are now accepted in programs.

As of now, "function", "predicate", "inductive", "val", "let", "fun",
and constructors in algebraic type declarations all accept the same
syntax for parameters. In "function", "predicate", "inductive", "val",
and constructors in algebraic type declarations, binders without
colons are treated as type expressions:

    function f int (list bool) (int,real) (ghost bool)

is syntactic sugar for

    function f (_: int) (_: list bool) (_: (int,real)) (ghost _: bool)

In "let" and "fun", single unqualified idents are treated as parameter
names whose types are to be inferred, other binders without colons are
treated as type expressions:

    let f int (list bool) (int,real) (ghost bool)

is syntactic sugar for

    let f (int: ?) (_: list bool) (_: (int,real)) (ghost bool: ?)

Anonymous binders ("_") are accepted only if their type is specified.

type point -> loc
predicate tree -> istree
post-condition: t -> t'

[<file.why>|<project directory> [<file.why> ...]]