Lean4
/-- Get the projections of a structure used by `@[simps]` applied to the appropriate arguments.
Returns a list of tuples
```
(corresponding right-hand-side, given projection name, projection Expression,
future projection numbers, used by default, is prefix)
```
(where all fields except the first are packed in a `ProjectionData` structure)
one for each projection. The given projection name is the name for the projection used by the user
used to generate (and parse) projection names. For example, in the structure
Example 1: ``getProjectionExprs env `(α × β) `(⟨x, y⟩)`` will give the output
```
[(`(x), `fst, `(@Prod.fst.{u v} α β), [], true, false),
(`(y), `snd, `(@Prod.snd.{u v} α β), [], true, false)]
```
Example 2: ``getProjectionExprs env `(α ≃ α) `(⟨id, id, fun _ ↦ rfl, fun _ ↦ rfl⟩)``
will give the output
```
[(`(id), `apply, (Equiv.toFun), [], true, false),
(`(id), `symm_apply, (fun e ↦ e.symm.toFun), [], true, false),
...,
...]
```
-/
def getProjectionExprs (stx : Syntax) (tgt : Expr) (rhs : Expr) (cfg : Config) :
MetaM <| Array <| Expr × ProjectionData := do
-- the parameters of the structure
let params := tgt.getAppArgs
if cfg.debug && !(← (params.zip rhs.getAppArgs).allM fun ⟨a, b⟩ ↦ isDefEq a b) then
throwError"unreachable code: parameters are not definitionally equal"
let str := tgt.getAppFn.constName?.getD default
let rhsArgs := rhs.getAppArgs.toList.drop params.size
let (rawUnivs, projDeclata) ← getRawProjections stx str
projDeclata.mapM fun proj ↦ do
let expr := proj.expr.instantiateLevelParams rawUnivs tgt.getAppFn.constLevels!
let proj := if ← isProof expr then { proj with isDefault := false } else proj
return
(rhsArgs.getD (fallback := default) proj.projNrs.head!,
{ proj with
expr := expr.instantiateLambdasOrApps params
projNrs := proj.projNrs.tail })
