Pipes for lambda clauses

[jonaprieto]

Add pipes instead of semicolons, as follows:

f : (A : Type) -> List A -> Nat;
f := \ {
     []        := 0
   | (x :: xs) := 1 + f xs
  };

[lukaszcz]

I just thought that maybe it's not so clear if we should have pipes here. Because one can see this also as analogous to a function definition where we end each clause with a semicolon. But on the other hand it does reflect the syntax of inductive types with the pipe. I don't know.