To be consistent with lean4, and to avoid confusion with function calls (we call my_function 3 4 and not my_function(3,4)), it would be better to support the following syntax:
def my_function (x:Int) (y:Int) : Int { x + y }
This syntax has another big advantage:
We can now replace refined types {x:Int | x > 0} with (x:Int | x > 0)
def my_function (x:Int | x > 0) (y:Int | y > x) : (z:Int | z < 1000) { x + y }
How to implement this feature:
[ ] Change the parser to accept multiple sets or arguments in parenthesis (trivial)
[ ] Automatically translate (x:Int | p) : Int to (x:{x:Int | p }) -> Int = \x ->
[ ] Change the type grammar rule to accept (x:Int | p) instead of {x : Int | p}
[ ] Add support to also accept (x:Int) instead of {x : Int | p}
Right now the syntax for arguments is:
To be consistent with lean4, and to avoid confusion with function calls (we call
my_function 3 4and notmy_function(3,4)), it would be better to support the following syntax:This syntax has another big advantage:
We can now replace refined types
{x:Int | x > 0}with(x:Int | x > 0)How to implement this feature:
(x:Int | p) : Intto(x:{x:Int | p }) -> Int = \x ->(x:Int | p)instead of{x : Int | p}(x:Int)instead of{x : Int | p}