Documentation

Init.Control.Option

instance instToBoolOption {α : Type u_1} :
Equations
  • instToBoolOption = { toBool := Option.toBool }
def OptionT (m : Type u → Type v) (α : Type u) :
Equations
Instances For
    @[inline]
    def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) :
    m (Option α)
    Equations
    Instances For
      def OptionT.mk {m : Type u → Type v} {α : Type u} (x : m (Option α)) :
      OptionT m α
      Equations
      Instances For
        @[inline]
        def OptionT.bind {m : Type u → Type v} [Monad m] {α : Type u} {β : Type u} (x : OptionT m α) (f : αOptionT m β) :
        OptionT m β
        Equations
        Instances For
          @[inline]
          def OptionT.pure {m : Type u → Type v} [Monad m] {α : Type u} (a : α) :
          OptionT m α
          Equations
          Instances For
            @[always_inline]
            instance OptionT.instMonadOptionT {m : Type u → Type v} [Monad m] :
            Equations
            • OptionT.instMonadOptionT = Monad.mk
            @[inline]
            def OptionT.orElse {m : Type u → Type v} [Monad m] {α : Type u} (x : OptionT m α) (y : UnitOptionT m α) :
            OptionT m α
            Equations
            Instances For
              @[inline]
              def OptionT.fail {m : Type u → Type v} [Monad m] {α : Type u} :
              OptionT m α
              Equations
              Instances For
                Equations
                • OptionT.instAlternativeOptionT = Alternative.mk (fun {α} => OptionT.fail) fun {α} => OptionT.orElse
                @[inline]
                def OptionT.lift {m : Type u → Type v} [Monad m] {α : Type u} (x : m α) :
                OptionT m α
                Equations
                Instances For
                  instance OptionT.instMonadLiftOptionT {m : Type u → Type v} [Monad m] :
                  Equations
                  • OptionT.instMonadLiftOptionT = { monadLift := fun {α} => OptionT.lift }
                  Equations
                  • OptionT.instMonadFunctorOptionT = { monadMap := fun {α} f x => f (Option α) x }
                  @[inline]
                  def OptionT.tryCatch {m : Type u → Type v} [Monad m] {α : Type u} (x : OptionT m α) (handle : UnitOptionT m α) :
                  OptionT m α
                  Equations
                  Instances For
                    Equations
                    • OptionT.instMonadExceptOfUnitOptionT = { throw := fun {α} x => OptionT.fail, tryCatch := fun {α} => OptionT.tryCatch }
                    instance OptionT.instMonadExceptOfOptionT {m : Type u → Type v} (ε : Type u) [Monad m] [MonadExceptOf ε m] :
                    Equations
                    instance instMonadControlOptionT {m : Type u_1 → Type u_2} [Monad m] :
                    Equations
                    • instMonadControlOptionT = { stM := Option, liftWith := fun {α} f => liftM (f fun {β} x => OptionT.run x), restoreM := fun {α} x => x }