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
Equations
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
    Equations
    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
      Equations
      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
        Equations
        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
          Equations
          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
            Equations
            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
              Equations
              Instances For
                source
                def Lean.mkNoConfusionEnum (enumName : Lake.Name) :
                Lean.MetaM Unit
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Lean.mkNoConfusionEnum.mkToCtorIdx (enumName : Lake.Name) :
                  Lean.MetaM Unit
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Lean.mkNoConfusionEnum.mkNoConfusionType (enumName : Lake.Name) :
                    Lean.MetaM Unit
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Lean.mkNoConfusionEnum.mkNoConfusion (enumName : Lake.Name) :
                      Lean.MetaM Unit
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Lean.mkNoConfusion (declName : Lake.Name) :
                        Lean.MetaM Unit
                        Equations
                        Instances For