@[extern lean_mk_cases_on]

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

@[extern lean_mk_no_confusion_type]

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

@[extern lean_mk_no_confusion]

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

def Lean.mkCasesOn (declName : Lake.Name) : Lean.MetaM Unit

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.mkNoConfusion (declName : Lake.Name) : Lean.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