Alternative notation for tuples and records, using bars instead of commas

[mikeshulman]

This is a proposal. I'm not 100% set on it yet, but in doing some more substantive coding with records I wasn't entirely happy with the current notation when it spans over multiple lines, and I think I like this better. This change allows you to write

def Magma : Type ≔ sig (
| t : Type
| op : t → t → t
)

and

def nat.magma : Magma ≔ (
| t ≔ ℕ
| op ≔ plus
)

the bars paralleling the notation for data, codata, match, and comatch. Commas are still also allowed; I prefer them for short inline tuples like (0,0).