Documentation

Lean.Meta.Constructions

source
@[extern lean_mk_cases_on]
opaque Lean.mkCasesOnImp (env : Lean.Environment) (declName : Lake.Name) :
Except Lean.KernelException Lean.Environment
source
@[extern lean_mk_rec_on]
opaque Lean.mkRecOnImp (env : Lean.Environment) (declName : Lake.Name) :
Except Lean.KernelException Lean.Environment
source
@[extern lean_mk_no_confusion]
opaque Lean.mkNoConfusionCoreImp (env : Lean.Environment) (declName : Lake.Name) :
Except Lean.KernelException Lean.Environment
source
@[extern lean_mk_below]
opaque Lean.mkBelowImp (env : Lean.Environment) (declName : Lake.Name) :
Except Lean.KernelException Lean.Environment
source
@[extern lean_mk_ibelow]
opaque Lean.mkIBelowImp (env : Lean.Environment) (declName : Lake.Name) :
Except Lean.KernelException Lean.Environment
source
@[extern lean_mk_brec_on]
opaque Lean.mkBRecOnImp (env : Lean.Environment) (declName : Lake.Name) :
Except Lean.KernelException Lean.Environment
source
@[extern lean_mk_binduction_on]
opaque Lean.mkBInductionOnImp (env : Lean.Environment) (declName : Lake.Name) :
Except Lean.KernelException Lean.Environment
source
def Lean.mkCasesOn {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) :
m Unit
Instances For
    source
    def Lean.mkRecOn {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) :
    m Unit
    Instances For
      source
      def Lean.mkNoConfusionCore {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) :
      m Unit
      Instances For
        source
        def Lean.mkBelow {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) :
        m Unit
        Instances For
          source
          def Lean.mkIBelow {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) :
          m Unit
          Instances For
            source
            def Lean.mkBRecOn {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) :
            m Unit
            Instances For
              source
              def Lean.mkBInductionOn {m : Type → Type} [Monad m] [Lean.MonadEnv m] [Lean.MonadError m] [Lean.MonadOptions m] (declName : Lake.Name) :
              m Unit
              Instances For
                source
                def Lean.mkNoConfusionEnum (enumName : Lake.Name) :
                Lean.MetaM Unit
                Instances For
                  source
                  def Lean.mkNoConfusionEnum.mkToCtorIdx (enumName : Lake.Name) :
                  Lean.MetaM Unit
                  Instances For
                    source
                    def Lean.mkNoConfusionEnum.mkNoConfusionType (enumName : Lake.Name) :
                    Lean.MetaM Unit
                    Instances For
                      source
                      def Lean.mkNoConfusionEnum.mkNoConfusion (enumName : Lake.Name) :
                      Lean.MetaM Unit
                      Instances For
                        source
                        def Lean.mkNoConfusion (declName : Lake.Name) :
                        Lean.MetaM Unit
                        Instances For