@[extern lean_mk_no_confusion_type]

opaque Lean.mkNoConfusionTypeCoreImp (env : Environment) (declName : Name) : Except KernelException Declaration

@[extern lean_mk_no_confusion]

opaque Lean.mkNoConfusionCoreImp (env : Environment) (declName : Name) : Except KernelException Declaration

def Lean.mkNoConfusionCore (declName : Name) : MetaM Unit

Equations

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

def Lean.mkNoConfusionEnum (enumName : Name) : MetaM Unit

Equations

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

def Lean.mkNoConfusionEnum.mkToCtorIdx (enumName : Name) : MetaM Unit

Equations

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

def Lean.mkNoConfusionEnum.mkNoConfusionType (enumName : Name) : MetaM Unit

Equations

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

def Lean.mkNoConfusionEnum.mkNoConfusion (enumName : Name) : MetaM Unit

Equations

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

def Lean.mkNoConfusion (declName : Name) : MetaM Unit

Equations

• Lean.mkNoConfusion declName = do let __do_lift ← Lean.isEnumType declName if __do_lift = true then Lean.mkNoConfusionEnum declName else Lean.mkNoConfusionCore declName