Documentation

Lean.Data.LOption

inductive Lean.LOption (α : Type u) :
Instances For
    instance Lean.instInhabitedLOption {a✝ : Type u_1} :
    Equations
      instance Lean.instBEqLOption {α✝ : Type u_1} [BEq α✝] :
      BEq (LOption α✝)
      Equations
        instance Lean.instToStringLOption {α : Type u_1} [ToString α] :
        Equations
          def Lean.LOption.toOption {α : Type u_1} :
          LOption αOption α
          Equations
            Instances For
              def Option.toLOption {α : Type u} :
              Equations
                Instances For
                  @[inline]
                  def toLOptionM {α : Type} {m : TypeType} [Monad m] (x : m (Option α)) :
                  Equations
                    Instances For