max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove OptionM

Browse source
This commit is contained in:
Leonardo de Moura 2022-05-04 15:30:10 -07:00
parent eaea5c4773
commit 5aaccc8ebb
1 changed files with 0 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/Control/Option.lean
View file

@ -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