Notation and term elaborators

In logic, semantics, and type systems (at least!), we encounter often the situation where we'd like to use important Lean symbols for notation. Examples: T → T for arrow types (functions) in an embedded type system, A → B for implication in an embedded logic, M → N for a reduction, x : T for x has type T, etc.

We will also need to combine notations in nontrivial ways. For example, this is the shape of reductions between typing judgements used in plenty of papers: (Γ ⊢ M : T) → (Γ ⊢ M' : T).

In a Zulip discussion (#computer science > Overloading Lean's notation), we discussed the possibility of using term elaborators. This is an example from Iris: https://github.com/leanprover-community/iris-lean/blob/master/src/Iris/BI/Notation.lean.
Thus we could write things like red(ty(Γ ⊢ M : T) → ty(Γ ⊢ M' : T)) (the nested ty might be unnecessary).

The design of these elaborators will need some thinking, so I'm opening this issue to keep record.