-
Andrei Paskevich authored
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.
ac5e027d