@[extern lean_mk_cases_on]

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

@[extern lean_mk_rec_on]

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

@[extern lean_mk_no_confusion]

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

@[extern lean_mk_below]

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

@[extern lean_mk_ibelow]

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

@[extern lean_mk_brec_on]

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

@[extern lean_mk_binduction_on]

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

def Lean.mkCasesOn {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) : m Unit

Equations

• Lean.mkCasesOn declName = Lean.adaptFn Lean.mkCasesOnImp declName

def Lean.mkRecOn {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) : m Unit

Equations

• Lean.mkRecOn declName = Lean.adaptFn Lean.mkRecOnImp declName

def Lean.mkNoConfusionCore {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) : m Unit

Equations

• Lean.mkNoConfusionCore declName = Lean.adaptFn Lean.mkNoConfusionCoreImp declName

def Lean.mkBelow {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) : m Unit

Equations

• Lean.mkBelow declName = Lean.adaptFn Lean.mkBelowImp declName

def Lean.mkIBelow {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) : m Unit

Equations

• Lean.mkIBelow declName = Lean.adaptFn Lean.mkIBelowImp declName

def Lean.mkBRecOn {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) : m Unit

Equations

• Lean.mkBRecOn declName = Lean.adaptFn Lean.mkBRecOnImp declName

def Lean.mkBInductionOn {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) : m Unit

Equations

• Lean.mkBInductionOn declName = Lean.adaptFn Lean.mkBInductionOnImp declName

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