From 8b5d75a2dd6c40c26ef5cad6310332e9906f1ff4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Mar 2020 18:38:41 -0800 Subject: [PATCH] chore: missing space --- src/Init/Lean/Meta/Tactic/Util.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Meta/Tactic/Util.lean b/src/Init/Lean/Meta/Tactic/Util.lean index 154eacfb25..404f93afe4 100644 --- a/src/Init/Lean/Meta/Tactic/Util.lean +++ b/src/Init/Lean/Meta/Tactic/Util.lean @@ -37,7 +37,7 @@ mctx ← getMCtx; opts ← getOptions; pure $ ppGoal env mctx opts mvarId -@[inline] protected def orelse{α} (x y : MetaM α) : MetaM α := do +@[inline] protected def orelse {α} (x y : MetaM α) : MetaM α := do s ← get; catch x (fun _ => do restore s.env s.mctx s.postponed; y) instance Meta.hasOrelse {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩