Lean4
/-- Suppose we are given a structure `str` and a projection `proj`, that could be multiple nested
projections (separated by `_`), where each projection could be a projection of a parent structure.
This function returns an expression that is the composition of these projections and a
list of natural numbers, that are the projection numbers of the applied projections.
Note that this function is similar to elaborating dot notation, but it can do a little more.
Example: if we do
```
structure gradedFun (A : ℕ → Type*) where
toFun := ∀ i j, A i →+ A j →+ A (i + j)
initialize_simps_projections (toFun_toFun_toFun → myMul)
```
we will be able to generate the "projection"
`fun {A} (f : gradedFun A) (x : A i) (y : A j) ↦ ↑(↑(f.toFun i j) x) y`,
which projection notation cannot do. -/
def getCompositeOfProjections (structName : Name) (proj : String) : MetaM (Expr × Array Nat) := do
let strExpr ← mkConstWithLevelParams structName
let type ← inferType strExpr
forallTelescopeReducing type fun typeArgs _ ↦
withLocalDeclD `x (mkAppN strExpr typeArgs) fun e ↦
getCompositeOfProjectionsAux (proj ++ "_") e #[] <| typeArgs.push e
