Documentation

Lean.Meta.Constructions

source
@[extern lean_mk_cases_on]
opaque Lean.mkCasesOnImp (env : Lean.Environment) (declName : Lean.Name) :
Except Lean.KernelException Lean.Environment
source
@[extern lean_mk_rec_on]
opaque Lean.mkRecOnImp (env : Lean.Environment) (declName : Lean.Name) :
Except Lean.KernelException Lean.Environment
source
@[extern lean_mk_no_confusion]
opaque Lean.mkNoConfusionCoreImp (env : Lean.Environment) (declName : Lean.Name) :
Except Lean.KernelException Lean.Environment
source
@[extern lean_mk_below]
opaque Lean.mkBelowImp (env : Lean.Environment) (declName : Lean.Name) :
Except Lean.KernelException Lean.Environment
source
@[extern lean_mk_ibelow]
opaque Lean.mkIBelowImp (env : Lean.Environment) (declName : Lean.Name) :
Except Lean.KernelException Lean.Environment
source
@[extern lean_mk_brec_on]
opaque Lean.mkBRecOnImp (env : Lean.Environment) (declName : Lean.Name) :
Except Lean.KernelException Lean.Environment
source
@[extern lean_mk_binduction_on]
opaque Lean.mkBInductionOnImp (env : Lean.Environment) (declName : Lean.Name) :
Except Lean.KernelException Lean.Environment
source
def Lean.mkCasesOn {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :
m Unit
Equations
source
def Lean.mkRecOn {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :
m Unit
Equations
source
def Lean.mkNoConfusionCore {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :
m Unit
Equations
source
def Lean.mkBelow {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :
m Unit
Equations
source
def Lean.mkIBelow {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :
m Unit
Equations
source
def Lean.mkBRecOn {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :
m Unit
Equations
source
def Lean.mkBInductionOn {m : Type → Type} [inst : Monad m] [inst : Lean.MonadEnv m] [inst : Lean.MonadError m] [inst : Lean.MonadOptions m] (declName : Lean.Name) :
m Unit
Equations
source
def Lean.mkNoConfusionEnum (enumName : Lean.Name) :
Lean.MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.mkNoConfusionEnum.mkToCtorIdx (enumName : Lean.Name) :
Lean.MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.mkNoConfusionEnum.mkNoConfusionType (enumName : Lean.Name) :
Lean.MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.mkNoConfusionEnum.mkNoConfusion (enumName : Lean.Name) :
Lean.MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.mkNoConfusion (declName : Lean.Name) :
Lean.MetaM Unit
Equations