Documentation

Lean.Data.LOption

inductive Lean.LOption (α : Type u) :
Instances For
    instance Lean.instBEqLOption :
    {α : Type u_1} → [inst : BEq α] → BEq (Lean.LOption α)
    def Option.toLOption {α : Type u} :
    Instances For
      @[inline]
      def toLOptionM {α : Type} {m : TypeType} [Monad m] (x : m (Option α)) :
      Instances For