Generalized `reduceProjs`

Stream: metaprogramming / tactics

[Leni Aniva]

Is there a generalized version for this function that works on all structures?

def reduceProjs (e : Expr) : CoreM Expr := do
  Core.transform e (post := fun e => do
    if e.isProj then
      if e.projExpr!.isAppOfArity ``PProd.mk 4 || e.projExpr!.isAppOfArity ``And.intro 2 then
        if e.projIdx! == 0 then
          return .continue e.projExpr!.appFn!.appArg!
        else
          return .continue e.projExpr!.appArg!
    return .continue
  )

[Robin Arnez]

Something like

import Lean

open Lean Meta

def reduceProjs (e : Expr) : MetaM Expr := do
  Core.transform e (post := fun e => do
    match ← reduceProj? e with
    | none => return .continue
    | some e => return .visit e)