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
                                      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
                                                          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
                                                                  instance Lean.instMonadRecDepthMonadCacheTOfMonad {α : Type} {m : TypeType} {ω β : Type} [BEq α] [Hashable α] [Monad m] [STWorld ω m] [MonadRecDepth m] :
                                                                  Equations
                                                                    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
                                                                      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
                                                                              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
                                                                                  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
                                                                                      Instances For