suggestion from review

oops

oops

RELEASES.md

@@ -132,6 +132,8 @@ fact.def :
 
 * The change to the instance name algorithm (described above) can break projects that made use of the auto-generated names.
 
+* `Option.toMonad` has been renamed to `Option.getM` and the unneeded `[Monad m]` instance argument has been removed.
+
 v4.7.0
 ---------
 

src/Init/Data/Option/Basic.lean

@@ -13,10 +13,14 @@ namespace Option
 deriving instance DecidableEq for Option
 deriving instance BEq for Option
 
-def toMonad [Monad m] [Alternative m] : Option α → m α
+/-- Lifts an optional value to any `Alternative`, sending `none` to `failure`. -/
+def getM [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
+@[deprecated getM] def toMonad [Monad m] [Alternative m] : Option α → m α :=
+  getM
+
 @[inline] def toBool : Option α → Bool
   | some _ => true
   | none   => false