Mentions légales du service

Skip to content
  • Andrei Paskevich's avatar
    unify the syntax of binders in logic and programs · ac5e027d
    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