Lean4
/-- Find the indices of the projections that need to be applied to elaborate `$e.$projName`.
Example: If `e : α ≃+ β` and ``projName = `invFun`` then this returns `[0, 1]`, because the first
projection of `MulEquiv` is `toEquiv` and the second projection of `Equiv` is `invFun`. -/
def findProjectionIndices (strName projName : Name) : MetaM (List Nat) := do
let env ← getEnv
let some baseStr := findField? env strName projName |
throwError "{strName } has no field {projName} in parent structure"
let some fullProjName := getProjFnForField? env baseStr projName |
throwError "no such field {projName}"
let some pathToField := getPathToBaseStructure? env baseStr strName |
throwError "no such field {projName}"
let allProjs := pathToField ++ [fullProjName]
return allProjs.map (env.getProjectionFnInfo? · |>.get!.i)
