Documentation

Lean.Data.LOption

inductive Lean.LOption (α : Type u) :
Instances For
Equations
  • Lean.instInhabitedLOption = { default := Lean.LOption.none }
instance Lean.instBEqLOption {α✝ : Type u_1} [BEq α✝] :
Equations
  • Lean.instBEqLOption = { beq := Lean.beqLOption✝ }
Equations
  • One or more equations did not get rendered due to their size.
def Option.toLOption {α : Type u} :
Equations
@[inline]
def toLOptionM {α : Type} {m : TypeType} [Monad m] (x : m (Option α)) :
Equations