perf: make Except.bind and OptionT.bind abbreviations for lazy-delta reduction

src/Init/Control/Except.lean

@@ -62,12 +62,15 @@ then the result is the result of the second computation.
 
 This is the implementation of the `>>=` operator for `Except ε`.
 -/
-@[always_inline, inline]
-protected def bind (ma : Except ε α) (f : α → Except ε β) : Except ε β :=
+@[always_inline]
+protected abbrev bind (ma : Except ε α) (f : α → Except ε β) : Except ε β :=
   match ma with
   | Except.error err => Except.error err
   | Except.ok v      => f v
 
+set_option allowUnsafeReducibility true in
+attribute [semireducible] Except.bind
+
 /-- Returns `true` if the value is `Except.ok`, `false` otherwise. -/
 @[always_inline, inline]
 protected def toBool : Except ε α → Bool

src/Init/Control/Option.lean

@@ -45,12 +45,15 @@ protected def mk (x : m (Option α)) : OptionT m α :=
 /--
 Sequences two potentially-failing actions. The second action is run only if the first succeeds.
 -/
-@[always_inline, inline, expose]
-protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β := OptionT.mk do
+@[always_inline]
+protected abbrev bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β := OptionT.mk do
   match (← x) with
   | some a => f a
   | none   => pure none
 
+set_option allowUnsafeReducibility true in
+attribute [semireducible] OptionT.bind
+
 /--
 Succeeds with the provided value.
 -/