From c653292422d5cf53365d674d733d333d524542e8 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 9 Feb 2018 17:56:31 +0100 Subject: [PATCH] feat(init/category/monad_fail): make `m` in `fail` implicit --- library/init/category/monad_fail.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/init/category/monad_fail.lean b/library/init/category/monad_fail.lean index 3a07baaf94..0ab68ce5ab 100644 --- a/library/init/category/monad_fail.lean +++ b/library/init/category/monad_fail.lean @@ -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 }