From da73cbbdec8c0d661e6cf94d85f8d33fef9688df Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 9 Dec 2019 15:40:38 -0800
Subject: [PATCH] chore: add abbreviations for `monadLift`

---
 src/Init/Control/Lift.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Init/Control/Lift.lean b/src/Init/Control/Lift.lean
index 263adde8eb..2611c7f8d1 100644
--- a/src/Init/Control/Lift.lean
+++ b/src/Init/Control/Lift.lean
@@ -29,6 +29,8 @@ class HasMonadLiftT (m : Type u → Type v) (n : Type u → Type w) :=
 
 export HasMonadLiftT (monadLift)
 
+abbrev liftM := @monadLift
+
 /-- A coercion that may reduce the need for explicit lifting.
     Because of [limitations of the current coercion resolution](https://github.com/leanprover/Lean/issues/1402), this definition is not marked as a global instance and should be marked locally instead. -/
 @[reducible] def hasMonadLiftToHasCoe {m n} [HasMonadLiftT m n] {α} : HasCoe (m α) (n α) :=