Meta tools for working with bundled lambdas

Stream: lean4

[Tomas Skrivan]

I'm planning to write bunch of meta programming tools to deal with lambda functions that are bundled morphisms. What I mean by this? I want to work with expressions like:

λ (x : ArrayN Float m) => ⊞ i, ∑ j, A i j * x[j]

where ArrayN is fixed size array and the notation ⊞ i, f i creates ArrayN Float n for f : Fin n → Float

or expression like:

λ (f df : C∞(ℝⁿ, ℝ)) => λ x =>[C∞] ⟪∇ f x, ∇ df x⟫

where λ x =>[C∞] f x is a smooth function, C∞(ℝⁿ, ℝ), assuming f : ℝⁿ → ℝ can be proven to be smooth by a tactic similar to continuity.

In particular, I want to have generalizations of getAppFn, getAppArgs, mkAppM, headBeta, eta, lambdaTelescope and probably bunch of others.

I would like to make this mathlib friendly as much as possible and would appreciate some advice on what should I look out for. Also if someone else would find this useful I'm happy to accept feature requests.

What is the go-to reference on bundled morphisms? I'm aware of Use and abuse of instance parameters in the Lean mathematical library which I should read once again.

[Tomas Skrivan]

I have a duct-tapped prototype of these tools here

[Tomas Skrivan]

Another question, what would be the best way to register a new morphism type? For continuous map, I would expect to somehow register these three functionsContinuousMap, ContinousMap.mk, ContinousMap.toFun. One of the nice things is that ContinousMap.mk already has auto parameter that gets discharged by continuity.

It is not clear to me at all what should I do for RingHom.