Add default arguments

[janmasrovira]

• Closes Default values for arguments #2386

This PR implements default arguments as described in #2386.

Change list

1. Extension of concrete syntax to include default values in function definitions.
2. Generalization of NameSignature/Builder so that it can also be used with scoped syntax.
3. Adaptation of Internal.FromConcrete.NamedArguments so that we insert default values instead of holes when needed.
4. Adaptation of ArityChecking.Checker so that it inserts default values instead of holes when needed.

Limitations

1. default values cannot refer to previous arguments. E.g., the following is a scope error:

   f {n : Nat := 0} {m : Nat := n + 1} .... 
   

2. Only functions can have default values.
3. Ony arguments on the LHS of the : can have arguments. E.g., the following is not valid syntax:

   f : {n : Nat := 0} := ...
   

   This is probably what we want since we want default arguments to be associated with the name of a function rather than a type.

[paulcadman]

It looks like there's some issue with type checking the default values?

The following type checks:

type T := mkT;
type U := mkU;

g {a : T := mkU} : T := a;

[janmasrovira]

It looks like there's some issue with type checking the default values?

The following type checks:

type T := mkT;
type U := mkU;

g {a : T := mkU} : T := a;

Oops. Because g is not used the default value is never inserted and so it does not reach type checking.
Maybe we'll need to keep default values in the Internal language so we can check them

[janmasrovira]

@paulcadman now default values are typed checked even if they are not used. I've added a negative test for it.