diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean index ebdcb40e97..4bf6f19c8b 100644 --- a/src/Init/Control/Option.lean +++ b/src/Init/Control/Option.lean @@ -10,7 +10,7 @@ import Init.Control.Except universe u v -instance : ToBool (Option α) := ⟨Option.toBool⟩ +instance : ToBool (Option α) := ⟨Option.isSome⟩ def OptionT (m : Type u → Type v) (α : Type u) : Type v := m (Option α) diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean index e6344f0320..bd0d091feb 100644 --- a/src/Init/Data/Option/Basic.lean +++ b/src/Init/Data/Option/Basic.lean @@ -21,15 +21,13 @@ def getM [Alternative m] : Option α → m α @[deprecated getM] def toMonad [Monad m] [Alternative m] : Option α → m α := getM -@[inline] def toBool : Option α → Bool - | some _ => true - | none => false - /-- Returns `true` on `some x` and `false` on `none`. -/ @[inline] def isSome : Option α → Bool | some _ => true | none => false +@[deprecated isSome, inline] def toBool : Option α → Bool := isSome + /-- Returns `true` on `none` and `false` on `some x`. -/ @[inline] def isNone : Option α → Bool | some _ => false