chore: deprecate Option.toBool in favour of Option.isSome (#3866)
This commit is contained in:
parent
7a65bde3e3
commit
7c34b736fc
2 changed files with 3 additions and 5 deletions
|
|
@ -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 α)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue