def Lean.mkCtorIdxName (indName : Name) : Name

Equations

• Lean.mkCtorIdxName indName = indName.mkStr "ctorIdx"

def Lean.isCtorIdxCore? (env : Environment) (declName : Name) : Option InductiveVal

Equations

• Lean.isCtorIdxCore? env (indName.str "ctorIdx") = Lean.isInductiveCore? env indName
• Lean.isCtorIdxCore? env declName = none

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

Equations

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

def Lean.mkCtorIdx (indName : Name) : 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.