opaque backwards.linearNoConfusionType : Lean.Option Bool

@[extern lean_mk_no_confusion_type]

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

@[extern lean_mk_no_confusion]

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

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

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

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

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

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

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