Documentation

Init.Control.Option

instance instToBoolOption {α : Type u_1} :
Equations
  • instToBoolOption = { toBool := Option.isSome }
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
    • x.run = x
    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
        • x.bind f = OptionT.mk do let __do_liftx match __do_lift with | some a => f a | none => pure none
        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.instMonad {m : Type u → Type v} [Monad m] :
            Equations
            • OptionT.instMonad = 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
                instance OptionT.instAlternative {m : Type u → Type v} [Monad m] :
                Equations
                @[inline]
                def OptionT.lift {m : Type u → Type v} [Monad m] {α : Type u} (x : m α) :
                OptionT m α
                Equations
                Instances For
                  instance OptionT.instMonadLift {m : Type u → Type v} [Monad m] :
                  Equations
                  • OptionT.instMonadLift = { monadLift := fun {α : Type u} => OptionT.lift }
                  instance OptionT.instMonadFunctor {m : Type u → Type v} :
                  Equations
                  • OptionT.instMonadFunctor = { monadMap := fun {α : Type u} (f : {β : Type u} → m βm β) (x : OptionT m α) => f 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.instMonadExceptOfUnit = { throw := fun {α : Type u} (x : Unit) => OptionT.fail, tryCatch := fun {α : Type u} => OptionT.tryCatch }
                    instance OptionT.instMonadExceptOfOfMonad {m : Type u → Type v} (ε : Type u) [Monad m] [MonadExceptOf ε m] :
                    Equations
                    • One or more equations did not get rendered due to their size.
                    instance instMonadControlOptionTOfMonad {m : Type u_1 → Type u_2} [Monad m] :
                    Equations
                    • One or more equations did not get rendered due to their size.