def reduceCtorIdx : Lean.Meta.Simp.DSimproc

This simproc reduces T.ctorIdx (T.con …) to the constructor index. It does not take part in simp's discrimination tree index, so can be costly on large goals.

Equations

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