From 630dcf4cc1f913eeb28190cdee4ec680831535e5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 22 Oct 2020 18:34:43 -0700 Subject: [PATCH] chore: code convention --- src/Init/Control/Option.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean index d61f45a69c..248941446d 100644 --- a/src/Init/Control/Option.lean +++ b/src/Init/Control/Option.lean @@ -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,