Documentation

Lean.Exception

inductive Lean.Exception :

Exception type used in most Lean monads

  • error (ref : Syntax) (msg : MessageData) : Exception

    Error messages that are displayed to users. ref is used to provide position information.

  • internal (id : InternalExceptionId) (extra : KVMap := { }) : Exception

    Internal exceptions that are not meant to be seen by users. Examples: "postpone elaboration", "stuck at universe constraint", etc.

Instances For

    Convert exception into a structured message.

    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
          Instances
            def Lean.throwError {m : TypeType} {α : Type} [Monad m] [MonadError m] (msg : 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

              Tag used for unknown identifier messages. This tag is used by the 'import unknown identifier' code action to detect messages that should prompt the code action.

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

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

                Equations
                Instances For

                  Creates a MessageData that is tagged with unknownIdentifierMessageTag. This tag is used by the 'import unknown identifier' code action to detect messages that should prompt the code action. The end position of the range of an unknown identifier message should always point at the end of the unknown identifier.

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

                    Throw an unknown identifier error message that is tagged with unknownIdentifierMessageTag. The end position of the range of ref should always point at the unknown identifier. See also mkUnknownIdentifierMessage.

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

                      Throw an unknown constant error message. The end position of the range of ref should point at the unknown identifier. See also mkUnknownIdentifierMessage.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Lean.throwUnknownConstant {m : TypeType} {α : Type} [Monad m] [MonadError m] (constName : Name) :
                        m α

                        Throw an unknown constant error message. The end position of the range of the current reference should point at the unknown identifier. See also mkUnknownIdentifierMessage.

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

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

                          Equations
                          Instances For
                            def Lean.throwInterruptException {m : TypeType} {α : Type} [Monad m] [MonadError m] [MonadOptions m] :
                            m α

                            Throws an internal interrupt exception that skips standard catch clauses and should be caught only at the top level of elaboration.

                            Equations
                            Instances For

                              Returns true if the exception is an interrupt generated by checkInterrupted.

                              Equations
                              Instances For

                                Throw an error exception for the given kernel exception.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                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.
                                      def Lean.throwMaxRecDepthAt {m : TypeType} {α : Type} [MonadError m] (ref : Syntax) :
                                      m α

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

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      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] [MonadError m] [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