Documentation

Lean.Exception

inductive Lean.Exception :

Exception type used in most Lean monads

Instances For

    Convert exception into a structured message.

    Equations
    Instances For
      Equations
      Instances For

        Return syntax object providing position information for the exception. Recall that internal exceptions do not have position information.

        Equations
        Instances For

          Similar to AddMessageContext, but for error messages. The default instance just uses AddMessageContext. In error messages, we may want to provide additional information (e.g., macro expansion stack), and refine the (ref : Syntax).

          Instances
            def Lean.throwError {m : TypeType} {α : Type} [Monad m] [Lean.MonadError m] (msg : Lean.MessageData) :
            m α

            Throw an error exception using the given message data. The result of getRef is used as position information. Recall that getRef returns the current "reference" syntax.

            Equations
            Instances For
              def Lean.throwUnknownConstant {m : TypeType} {α : Type} [Monad m] [Lean.MonadError m] (constName : Lake.Name) :
              m α

              Throw an unknown constant error message.

              Equations
              Instances For
                def Lean.throwErrorAt {m : TypeType} {α : Type} [Monad m] [Lean.MonadError m] (ref : Lean.Syntax) (msg : Lean.MessageData) :
                m α

                Throw an error exception using the given message data and reference syntax.

                Equations
                Instances For
                  def Lean.ofExcept {m : TypeType} {ε : Type u_1} {α : Type} [Monad m] [Lean.MonadError m] [ToString ε] (x : Except ε α) :
                  m α

                  Convert an Except into a m monadic action, where m is any monad that implements MonadError.

                  Equations
                  Instances For

                    Throw an error exception for the given kernel exception.

                    Equations
                    Instances For

                      Lift from Except KernelException to m when m can throw kernel exceptions.

                      Equations
                      Instances For
                        class Lean.MonadRecDepth (m : TypeType) :
                        • withRecDepth : {α : Type} → Natm αm α
                        • getRecDepth : m Nat
                        • getMaxRecDepth : m Nat
                        Instances
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Equations
                          Equations
                          def Lean.throwMaxRecDepthAt {m : TypeType} {α : Type} [Lean.MonadError m] (ref : Lean.Syntax) :
                          m α

                          Throw a "maximum recursion depth has been reached" exception using the given reference syntax.

                          Equations
                          Instances For

                            Return true if ex was generated by throwMaxRecDepthAt. This function is a bit hackish. The max rec depth exception should probably be an internal exception, but it is also produced by MacroM which implemented in the prelude, and internal exceptions have not been defined yet.

                            Equations
                            Instances For
                              @[inline]
                              def Lean.withIncRecDepth {m : TypeType} {α : Type} [Monad m] [Lean.MonadError m] [Lean.MonadRecDepth m] (x : m α) :
                              m α

                              Increment the current recursion depth and then execute x. Throw an exception if maximum recursion depth has been reached. We use this combinator to prevent stack overflows.

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

                                Macro for throwing error exceptions. The argument can be an interpolated string. It is a convenient way of building MessageData objects. The result of getRef is used as position information. Recall that getRef returns the current "reference" syntax.

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

                                  Macro for throwing error exceptions. The argument can be an interpolated string. It is a convenient way of building MessageData objects. The first argument must be a Syntax that provides position information for the error message. throwErrorAt ref msg is equivalent to withRef ref <| throwError msg

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