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

chore: make tryFinally a def

Browse source
This commit is contained in:
Sebastian Ullrich 2021-02-17 12:04:20 +01:00
parent c0a3ea7c7e
commit 187a614575
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/Control/Except.lean
View file

@ -138,7 +138,7 @@ class MonadFinally (m : Type u → Type v) where
export MonadFinally (tryFinally')
/-- Execute `x` and then execute `finalizer` even if `x` threw an exception -/
@[inline] abbrev tryFinally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α :=
@[inline] def tryFinally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α :=
let y := tryFinally' x (fun _ => finalizer)
(·.1) <$> y