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

chore: code convention

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-22 18:34:43 -07:00
parent 29e8c42628
commit 630dcf4cc1
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -12,10 +12,10 @@ import Init.Control.Except
universes u v
def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
m (Option α)
m (Option α)
@[inline] def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) : m (Option α) :=
x
x
namespace OptionT
variables {m : Type u → Type v} [Monad m] {α β : Type u}
@ -54,8 +54,8 @@ instance : MonadLift m (OptionT m) := ⟨OptionT.lift⟩
instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩
@[inline] protected def tryCatch (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := id (α := m (Option α)) do
let some a ← x | handle ()
pure a
let some a ← x | handle ()
pure a
instance : MonadExceptOf Unit (OptionT m) := {
throw := fun _ => OptionT.fail,