Documentation

Lean.CoreM

Cache for the CoreM monad

Instances For
    Equations

    State for the CoreM monad.

    Instances For

      Context for the CoreM monad.

      Instances For
        @[inline, reducible]
        abbrev Lean.Core.CoreM (α : Type) :

        CoreM is a monad for manipulating the Lean environment. It is the base monad for MetaM. The main features it provides are:

        • name generator state
        • environment state
        • Lean options context
        • the current open namespace
        Equations
        Instances For
          Equations
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Equations
            • One or more equations did not get rendered due to their size.
            @[inline]
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[inline]
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[inline]
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[inline]
                      def Lean.Core.liftIOCore {α : Type} (x : IO α) :
                      Equations
                      Instances For
                        Equations
                        Equations
                        • One or more equations did not get rendered due to their size.

                        Restore backtrackable parts of the state.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[inline]
                          Equations
                          Instances For
                            @[inline]
                            Equations
                            Instances For
                              @[inline]
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                def Lean.Core.withIncRecDepth {m : TypeType u_1} {α : Type} [Monad m] [MonadControlT Lean.CoreM m] (x : m α) :
                                m α
                                Equations
                                Instances For
                                  @[inline]
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def Lean.Core.throwMaxHeartbeat (moduleName : Lake.Name) (optionName : Lake.Name) (max : Nat) :
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      def Lean.Core.checkMaxHeartbeatsCore (moduleName : String) (optionName : Lake.Name) (max : Nat) :
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Equations
                                        Instances For
                                          def Lean.Core.withCurrHeartbeats {m : TypeType u_1} {α : Type} [Monad m] [MonadControlT Lean.CoreM m] (x : m α) :
                                          m α
                                          Equations
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                Instances For
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  @[inline]
                                                  def Lean.withAtLeastMaxRecDepth {m : TypeType u_1} {α : Type} [MonadFunctorT Lean.CoreM m] (max : Nat) :
                                                  m αm α
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[inline]
                                                    def Lean.catchInternalId {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [MonadExcept Lean.Exception m] (id : Lean.InternalExceptionId) (x : m α) (h : Lean.Exceptionm α) :
                                                    m α
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[inline]
                                                      def Lean.catchInternalIds {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [MonadExcept Lean.Exception m] (ids : List Lean.InternalExceptionId) (x : m α) (h : Lean.Exceptionm α) :
                                                      m α
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        Return true if ex was generated by throwMaxHeartbeat. This function is a bit hackish. The heartbeat exception should probably be an internal exception. We used a similar hack at Exception.isMaxRecDepth

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For

                                                          Creates the expression d → b

                                                          Equations
                                                          Instances For
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[extern lean_lcnf_compile_decls]
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For

                                                                    Return true if the exception was generated by one our resource limits.

                                                                    Equations
                                                                    Instances For
                                                                      @[inline]

                                                                      Custom try-catch for all monads based on CoreM. We don't want to catch "runtime exceptions" in these monads, but on CommandElabM. See issues #2775 and #2744

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        Equations
                                                                        @[inline]
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[inline]
                                                                          def Lean.mapCoreM {m : TypeType u_1} [MonadControlT Lean.CoreM m] [Monad m] (f : {α : Type} → Lean.CoreM αLean.CoreM α) {α : Type} (x : m α) :
                                                                          m α
                                                                          Equations
                                                                          Instances For
                                                                            @[inline]
                                                                            def Lean.withCatchingRuntimeEx {m : TypeType u_1} {α : Type} [MonadControlT Lean.CoreM m] [Monad m] (x : m α) :
                                                                            m α

                                                                            Execute x with catchRuntimeEx = flag. That is, given try x catch ex => h ex, if x throws a runtime exception, the handler h will be invoked if flag = true Recall that

                                                                            Equations
                                                                            Instances For
                                                                              @[inline]
                                                                              def Lean.withoutCatchingRuntimeEx {m : TypeType u_1} {α : Type} [MonadControlT Lean.CoreM m] [Monad m] (x : m α) :
                                                                              m α
                                                                              Equations
                                                                              Instances For