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

chore: remove temporary def

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-22 17:42:17 -07:00
parent 2389b6dc92
commit a0b8f13094
1 changed files with 0 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Control/Except.lean
View file

@ -196,10 +196,6 @@ export MonadFinally (tryFinally')
@[inline] abbrev tryFinally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α := do
Prod.fst <$> tryFinally' x (fun _ => finalizer)
-- TODO delete
@[inline] abbrev finally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α := do
Prod.fst <$> tryFinally' x (fun _ => finalizer)
instance Id.finally : MonadFinally Id :=
{ tryFinally' := fun α β x h =>
let a := x;