Documentation

Init.Control.Except

@[inline]
def Except.pure {ε : Type u} {α : Type u_1} (a : α) :
Except ε α
Equations
Instances For
    @[inline]
    def Except.map {ε : Type u} {α : Type u_1} {β : Type u_2} (f : αβ) :
    Except ε αExcept ε β
    Equations
    Instances For
      @[simp]
      theorem Except.map_id {ε : Type u} {α : Type u_1} :
      @[inline]
      def Except.mapError {ε : Type u} {ε' : Type u_1} {α : Type u_2} (f : εε') :
      Except ε αExcept ε' α
      Equations
      Instances For
        @[inline]
        def Except.bind {ε : Type u} {α : Type u_1} {β : Type u_2} (ma : Except ε α) (f : αExcept ε β) :
        Except ε β
        Equations
        Instances For
          @[inline]
          def Except.toBool {ε : Type u} {α : Type u_1} :
          Except ε αBool

          Returns true if the value is Except.ok, false otherwise.

          Equations
          Instances For
            @[inline, reducible]
            abbrev Except.isOk {ε : Type u} {α : Type u_1} :
            Except ε αBool
            Equations
            • Except.isOk = Except.toBool
            Instances For
              @[inline]
              def Except.toOption {ε : Type u} {α : Type u_1} :
              Except ε αOption α
              Equations
              Instances For
                @[inline]
                def Except.tryCatch {ε : Type u} {α : Type u_1} (ma : Except ε α) (handle : εExcept ε α) :
                Except ε α
                Equations
                Instances For
                  def Except.orElseLazy {ε : Type u} {α : Type u_1} (x : Except ε α) (y : UnitExcept ε α) :
                  Except ε α
                  Equations
                  Instances For
                    @[always_inline]
                    instance Except.instMonadExcept {ε : Type u} :
                    Equations
                    • Except.instMonadExcept = Monad.mk
                    def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) :
                    Equations
                    Instances For
                      @[inline]
                      def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) :
                      ExceptT ε m α
                      Equations
                      Instances For
                        @[inline]
                        def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) :
                        m (Except ε α)
                        Equations
                        Instances For
                          @[inline]
                          def ExceptT.pure {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (a : α) :
                          ExceptT ε m α
                          Equations
                          Instances For
                            @[inline]
                            def ExceptT.bindCont {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (f : αExceptT ε m β) :
                            Except ε αm (Except ε β)
                            Equations
                            Instances For
                              @[inline]
                              def ExceptT.bind {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (ma : ExceptT ε m α) (f : αExceptT ε m β) :
                              ExceptT ε m β
                              Equations
                              Instances For
                                @[inline]
                                def ExceptT.map {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (f : αβ) (x : ExceptT ε m α) :
                                ExceptT ε m β
                                Equations
                                Instances For
                                  @[inline]
                                  def ExceptT.lift {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (t : m α) :
                                  ExceptT ε m α
                                  Equations
                                  Instances For
                                    @[always_inline]
                                    instance ExceptT.instMonadLiftExceptExceptT {ε : Type u} {m : Type u → Type v} [Monad m] :
                                    Equations
                                    • ExceptT.instMonadLiftExceptExceptT = { monadLift := fun {α} e => ExceptT.mk (pure e) }
                                    instance ExceptT.instMonadLiftExceptT {ε : Type u} {m : Type u → Type v} [Monad m] :
                                    Equations
                                    • ExceptT.instMonadLiftExceptT = { monadLift := fun {α} => ExceptT.lift }
                                    @[inline]
                                    def ExceptT.tryCatch {ε : Type u} {m : Type u → Type v} [Monad m] {α : Type u} (ma : ExceptT ε m α) (handle : εExceptT ε m α) :
                                    ExceptT ε m α
                                    Equations
                                    Instances For
                                      instance ExceptT.instMonadFunctorExceptT {ε : Type u} {m : Type u → Type v} :
                                      Equations
                                      • ExceptT.instMonadFunctorExceptT = { monadMap := fun {α} f x => f (Except ε α) x }
                                      @[always_inline]
                                      instance ExceptT.instMonadExceptT {ε : Type u} {m : Type u → Type v} [Monad m] :
                                      Monad (ExceptT ε m)
                                      Equations
                                      • ExceptT.instMonadExceptT = Monad.mk
                                      @[inline]
                                      def ExceptT.adapt {ε : Type u} {m : Type u → Type v} [Monad m] {ε' : Type u} {α : Type u} (f : εε') :
                                      ExceptT ε m αExceptT ε' m α
                                      Equations
                                      Instances For
                                        @[always_inline]
                                        instance instMonadExceptOfExceptT (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] :
                                        MonadExceptOf ε₁ (ExceptT ε₂ m)
                                        Equations
                                        @[always_inline]
                                        instance instMonadExceptOfExceptT_1 (m : Type u → Type v) (ε : Type u) [Monad m] :
                                        Equations
                                        instance instInhabitedExceptT {m : Type u_1 → Type u_2} {ε : Type u_1} {α : Type u_1} [Monad m] [Inhabited ε] :
                                        Inhabited (ExceptT ε m α)
                                        Equations
                                        • instInhabitedExceptT = { default := throw default }
                                        instance instMonadExceptOfExcept (ε : Type u_1) :
                                        Equations
                                        @[inline]
                                        def MonadExcept.orelse' {ε : Type u} {m : Type v → Type w} [MonadExcept ε m] {α : Type v} (t₁ : m α) (t₂ : m α) (useFirstEx : optParam Bool true) :
                                        m α

                                        Alternative orelse operator that allows to select which exception should be used. The default is to use the first exception since the standard orelse uses the second.

                                        Equations
                                        Instances For
                                          @[inline]
                                          def observing {ε : Type u} {α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) :
                                          m (Except ε α)
                                          Equations
                                          Instances For
                                            def liftExcept {ε : Type u_1} {m : Type u_2 → Type u_3} {α : Type u_2} [MonadExceptOf ε m] [Pure m] :
                                            Except ε αm α
                                            Equations
                                            Instances For
                                              instance instMonadControlExceptT (ε : Type u) (m : Type u → Type v) [Monad m] :
                                              Equations
                                              class MonadFinally (m : Type u → Type v) :
                                              Type (max (u + 1) v)
                                              • tryFinally' : {α β : Type u} → m α(Option αm β) → m (α × β)

                                                tryFinally' x f runs x and then the "finally" computation f. When x succeeds with a : α, f (some a) is returned. If x fails for m's definition of failure, f none is returned. Hence tryFinally' can be thought of as performing the same role as a finally block in an imperative programming language.

                                              Instances
                                                @[inline]
                                                def tryFinally {m : Type u → Type v} {α : Type u} {β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) :
                                                m α

                                                Execute x and then execute finalizer even if x threw an exception

                                                Equations
                                                Instances For
                                                  @[always_inline]
                                                  Equations
                                                  • Id.finally = { tryFinally' := fun {α β} x h => let a := x; let b := h (some x); pure (a, b) }
                                                  @[always_inline]
                                                  instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m] [Monad m] :
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.