Default values for arguments

[janmasrovira]

• We discussed in Optional and named arguments #1991 (comment) the idea to allow default values for implicit arguments.
  Iirc the syntax that we agreed online was as follows:

f {x : Nat := 0} : {y : Nat := 1} -> Nat := x + y;

Semantically, when we would insert a hole for an implicit argument that has a default value, we insert the default value instead.

• It is generally useful thing to have. In particular, it would be useful for Proposal: Use a Juvix source file to define a package instead of YAML #2336.