Add syntax support for record updates

[jonaprieto]

type A (B : Type) :=
  constructorName {
    cfield1 : X1;
    cfield2 : X2;
 };

An update for A is written as follows:

f : A B;
f := constructorName { cfield1 := x; cfield2 := y};

g : A B -> A B;
g r := r { cfield1 := x};

[lukaszcz]

The above record update syntax doesn't play well with the proposed syntax for named arguments:

• Optional and named arguments #1991.

Named arguments automatically provide record creation syntax:

constructorName (cfield1 := x; cfield2 := y)

is just

constructorName x y

But then

r {cfield1 := x}

would desugar to

r {x}

and this conflicts with the record update syntax.

I propose to introduce a keyword with for record updates:

r with {cfield1 := x}

[lukaszcz]

I think it would be convenient, especially in combination with traits, to also allow with for record creation, and allow full top-level declaration syntax including optional signatures inside the braces on the right. Then given a trait:

trait
type Encoding (A : Type) := MkEncoding {
  encode : A -> Field;
  decode : Field -> A;
};

one could write:

type E (A : Type) := 
| C1 : A -> E 
| C2 : E;

instance 
encoding : {A : Type} -> {{Encoding A}} -> Encoding (E A);
encoding := MkEncoding with {
  encode : E A -> Field;
  encode (C1 x) := encode x + 1;
  encode C2 := 0;

  decode : Field -> E A;
  decode zero := C2; 
  decode (suc x) := C1 (decode x);
};

[janmasrovira]

I think adding the with keyword to remove ambiguity is reasonable.
I also like the proposal to allow inline function definitions in record creation/update.