Documentation

Lean.Meta.Tactic.Grind.CtorIdx

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

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

Equations
    Instances For