def mkToCtorIdxName (indName : Lean.Name) : Lean.Name

Equations

• mkToCtorIdxName indName = indName.mkStr "toCtorIdx"

def mkCtorIdxName (indName : Lean.Name) : Lean.Name

Equations

• mkCtorIdxName indName = indName.mkStr "ctorIdx"

def mkCtorIdx (indName : Lean.Name) : Lean.MetaM Unit

For an inductive type T with more than one function builds a function T.ctorIdx : T → Nat that returns the constructor index of the given value. Does nothing if T does not eliminate into Type or if T is unsafe. Assumes T.casesOn to be defined already.

Equations

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