Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]

[Peter Hancock]

It may be of no general interest, but an an informal level I very often use
a notation for functions like, fairly smoothly,
likethat which I think is being discussed in this thread.
I generally use

    [ c1 p11 .. p1k_1 |-> ... | ... ] : (x : Coprod)  -> ... x ...

using `|->' for the symbol that segregates a (linear) pattern from the corresponding
rhs, which may contain the variables of the pattern.  I call this co-tuple notation,
when there is more than one |-separated "arm", and functional abstraction when the pattern is empty.

I also use (x |-> .. x ..) for simple functional abstraction, occasionally
( x : A |-> .. x .. ) if I want to show the type of the domain,
( x : A |-> .. x .. : B x) if the codomain is also interesting.

I think I learnt this use of `|->' from the specification language Z, which
seemed to have a coherent systematic account of it.  The square brackets I
picked up from Lamport's TLA.

I'd like also to come out of the syntax-closet (blush), and admit to being fascinated
by the idea of pattern matching at function types, as in the declaration

   (s : S |-> (C s : Set, c |-> (R s c, r |-> n s c r))) : S -> Fam^2 S,, ...

where higher-order variables C, R and n are introduced by by pattern matching
(and Fam X = (Sigma I : Set) I -> X).   I can't recall anything going wrong when
using this way of introducing variables via patterns, *unless* variables are repeated,
which I suspect is really propositional equality in disguise.

Hank