def Lean.Meta.Grind.propagateCtorIdxUp (e : Expr) : GoalM Unit

Propagation for T.ctorIdx. Cf. the reduceCtorIdx simproc.

Equations

• One or more equations did not get rendered due to their size.