diff --git a/src/Init/Lean/Elab/Level.lean b/src/Init/Lean/Elab/Level.lean
index 3b200766f4..eaab7ee8ed 100644
--- a/src/Init/Lean/Elab/Level.lean
+++ b/src/Init/Lean/Elab/Level.lean
@@ -81,5 +81,8 @@ partial def elabLevel : Syntax → LevelElabM Level
     throwError stx "unexpected universe level syntax kind"
 
 end Level
+
+export Level (LevelElabM)
+
 end Elab
 end Lean
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index c5643ce867..0eb2b8042b 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -11,6 +11,7 @@ import Init.Lean.Hygiene
 import Init.Lean.Elab.Log
 import Init.Lean.Elab.Alias
 import Init.Lean.Elab.ResolveName
+import Init.Lean.Elab.Level
 
 namespace Lean
 namespace Elab
@@ -262,6 +263,15 @@ match u? with
 | some u => pure u
 | none   => throwError ref ("invalid universe level, " ++ u ++ " is not greater than 0")
 
+def liftLevelM {α} (x : LevelElabM α) : TermElabM α :=
+fun ctx s =>
+  match (x { .. ctx }).run { .. s } with
+  | EStateM.Result.ok a newS     => EStateM.Result.ok a { mctx := newS.mctx, ngen := newS.ngen, .. s }
+  | EStateM.Result.error ex newS => EStateM.Result.error (Exception.error ex) s
+
+def elabLevel (stx : Syntax) : TermElabM Level :=
+liftLevelM $ Level.elabLevel stx
+
 /- Elaborate `x` with `stx` on the macro stack -/
 @[inline] def withMacroExpansion {α} (stx : Syntax) (x : TermElabM α) : TermElabM α :=
 adaptReader (fun (ctx : Context) => { macroStack := stx :: ctx.macroStack, .. ctx }) x