Alternative dot notation

[YaelDillies]

Use of dot notation (aka projection) is currently restricted on two aspects:

• It resolves linearly by unfolding definitions.
• We can't use it on built-ins.

One way to solve both problems would be to introduce a command dot_alias which would declare aliases dot notation can resolve to.

For example, dot_alias function := a → b (syntax to be determined), means that h.comp could resolve to function.comp h where h : a → b. And similarly, we could add the aliases pi and imp for Π i, α i.

Note: I'm not sure whether this belongs here or in the Lean repo.

[kmill]

leanprover-community/lean#757 gave the ability to do h.comp using the function namespace.

We can't change how dot notation works from within mathlib, and I don't think we'll see any more development on dot notation for Lean 3, so I'll go ahead and close this.