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

chore: missing space

Browse source
This commit is contained in:
Leonardo de Moura 2020-03-05 18:38:41 -08:00
parent 35000ff4cd
commit 8b5d75a2dd
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Meta/Tactic/Util.lean
View file

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