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 isCtorIdxCore? (env : Lean.Environment) (declName : Lean.Name) : Option Lean.InductiveVal

Equations

• isCtorIdxCore? env (indName.str "ctorIdx") = do let indInfo ← Lean.isInductiveCore? env indName pure indInfo
• isCtorIdxCore? env declName = none

def isCtorIdx? (declName : Lean.Name) : Lean.MetaM (Option Lean.InductiveVal)

Equations

• isCtorIdx? declName = do let __do_lift ← Lean.getEnv pure (isCtorIdxCore? __do_lift declName)

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.