Named arguments

[janmasrovira]

• closes Optional and named arguments #1991

This pr implements named arguments as described in #1991. It does not yet implement optional arguments, which should be added in a later pr as they are not required for record syntax.

Syntax Overview

Named arguments are a convenient mehcanism to provide arguments, where we give the arguments by name instead of by position. Anything with a type signature can have named arguments, i.e. functions, types, constructors and axioms.

For instance, if we have (note that named arguments can also appear on the rhs of the :):

fun : {A B : Type} (f : A -> B) : (x : A) -> B := ... ;

With the traditional positional application, we would write

fun suc zero

With named arguments we can write the following:

1. fun (f := suc) (x := zero).
2. We can change the order: fun (x := zero) (f := suc).
3. We can group the arguments: fun (x := zero; f := suc).
4. We can partially apply functions with named arguments: fun (f := suc) zero.
5. We can provide implicit arguments analogously (with braces): fun {A := Nat; B := Nat} (f := suc; x := zero).
6. We can skip implicit arguments: fun {B := Nat} (f := suc; x := zero).

What we cannot do:

1. Skip explicit arguments. E.g. fun (x := zero).
2. Mix explicit and implicit arguments in the same group. E.g. fun (A := Nat; f := suc)
3. Provide explicit and implicit arguments in different order. E.g. fun (f := suc; x := zero) {A := Nat}.

[paulcadman]

🌟