From 5aaccc8ebba4cf69f9975d240dad41f4f2a91ec5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 May 2022 15:30:10 -0700 Subject: [PATCH] chore: remove `OptionM` --- src/Init/Control/Option.lean | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean index 5a36ff7014..8b587200d4 100644 --- a/src/Init/Control/Option.lean +++ b/src/Init/Control/Option.lean @@ -69,11 +69,6 @@ instance (ε : Type u) [Monad m] [MonadExceptOf ε m] : MonadExceptOf ε (Option end OptionT -abbrev OptionM (α : Type u) := OptionT Id α - -abbrev OptionM.run (x : OptionM α) : Option α := - x - instance [Monad m] : MonadControl m (OptionT m) where stM := Option liftWith f := liftM <| f fun x => x.run