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

feat(init/category/monad_fail): make m in fail implicit

Browse source
This commit is contained in:
Sebastian Ullrich 2018-02-09 17:56:31 +01:00 • committed by Leonardo de Moura
parent ace8ef286a
commit c653292422
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/category/monad_fail.lean
View file

@ -9,14 +9,14 @@ import init.category.transformers init.data.string.basic
universes u v
class monad_fail (m : Type u → Type v) extends monad m :=
(fail : Π {a}, string → m a)
(fail {} : Π {a}, string → m a)
-- deriving monad from monad_fail should happen only as a last resort
attribute [instance, priority 1] monad_fail.to_monad
def match_failed {α : Type u} {m : Type u → Type v} [monad_fail m] : m α :=
monad_fail.fail m "match failed"
monad_fail.fail "match failed"
-- TODO(Sebastian): Could take `has_monad_lift_t`, except that the refl instances will make it loop
instance monad_fail_lift (m n : Type u → Type v) [has_monad_lift m n] [monad_fail m] [monad_n : monad n] : monad_fail n :=
{ fail := λ α s, monad_lift (monad_fail.fail m s : m α), ..monad_n }
{ fail := λ α s, monad_lift (monad_fail.fail s : m α), ..monad_n }