diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 44a5652fe8..f13e1dd589 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -227,7 +227,7 @@ delabFor k <|> (liftM $ show MetaM Syntax from throwError $ "don't know how to d
 @[builtinDelab fvar]
 def delabFVar : Delab := do
 Expr.fvar id _ ← getExpr | unreachable!;
-l ← liftM $ getLocalDecl id;
+l ← getLocalDecl id;
 pure $ mkIdent l.userName
 
 @[builtinDelab mvar]
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index e99c8d0df3..726fa76ea4 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -164,7 +164,7 @@ def elabBinders {α} (binders : Array Syntax) (x : Array Expr → TermElabM α)
 if binders.isEmpty then x #[]
 else do
   lctx ← getLCtx;
-  localInsts ← getLocalInsts;
+  localInsts ← getLocalInstances;
   (fvars, lctx, newLocalInsts) ← elabBindersAux binders 0 #[] lctx localInsts;
   resettingSynthInstanceCacheWhen (newLocalInsts.size > localInsts.size) $ withLCtx lctx newLocalInsts $
     x fvars
@@ -177,7 +177,7 @@ fun stx _ => match_syntax stx with
 | `(forall $binders*, $term) =>
   elabBinders binders $ fun xs => do
     e ← elabType term;
-    mkForall xs e
+    mkForallFVars xs e
 | _ => throwUnsupportedSyntax
 
 @[builtinTermElab arrow] def elabArrow : TermElab :=
@@ -192,7 +192,7 @@ fun stx _ =>
   let term   := stx.getArg 2;
   elabBinders #[binder] $ fun xs => do
     e ← elabType term;
-    mkForall xs e
+    mkForallFVars xs e
 
 /-- Main loop `getFunBinderIds?` -/
 private partial def getFunBinderIdsAux? : Bool → Syntax → Array Syntax → TermElabM (Option (Array Syntax))
@@ -352,7 +352,7 @@ def elabFunBinders {α} (binders : Array Syntax) (expectedType? : Option Expr) (
 if binders.isEmpty then x #[] expectedType?
 else do
   lctx ← getLCtx;
-  localInsts ← getLocalInsts;
+  localInsts ← getLocalInstances;
   s ← FunBinders.elabFunBindersAux binders 0 { lctx := lctx, localInsts := localInsts, expectedType? := expectedType? };
   resettingSynthInstanceCacheWhen (s.localInsts.size > localInsts.size) $ withLCtx s.lctx s.localInsts $
     x s.fvars s.expectedType?
@@ -369,7 +369,7 @@ if expandedPattern then do
 else
   elabFunBinders binders expectedType? $ fun xs expectedType? => do
     e ← elabTerm body expectedType?;
-    mkLambda xs e
+    mkLambdaFVars xs e
 
 /-
   Recall that
@@ -390,8 +390,8 @@ def elabLetDeclAux (n : Name) (binders : Array Syntax) (typeStx : Syntax) (valSt
 (type, val) ← elabBinders binders $ fun xs => do {
   type ← elabType typeStx;
   val  ← elabTermEnsuringType valStx type;
-  type ← mkForall xs type;
-  val  ← mkLambda xs val;
+  type ← mkForallFVars xs type;
+  val  ← mkLambdaFVars xs val;
   pure (type, val)
 };
 trace `Elab.let.decl $ fun _ => n ++ " : " ++ type ++ " := " ++ val;
@@ -399,12 +399,12 @@ if useLetExpr then
   withLetDecl n type val $ fun x => do
     body ← elabTerm body expectedType?;
     body ← instantiateMVars body;
-    mkLet x body
+    mkLetFVars #[x] body
 else do
   f ← withLocalDecl n BinderInfo.default type $ fun x => do {
     body ← elabTerm body expectedType?;
     body ← instantiateMVars body;
-    mkLambda #[x] body
+    mkLambdaFVars #[x] body
   };
   pure $ mkApp f val
 
diff --git a/src/Lean/Elab/CollectFVars.lean b/src/Lean/Elab/CollectFVars.lean
index 6607de7260..da33baca5b 100644
--- a/src/Lean/Elab/CollectFVars.lean
+++ b/src/Lean/Elab/CollectFVars.lean
@@ -11,24 +11,24 @@ namespace Elab
 namespace Term
 
 def collectUsedFVars (used : CollectFVars.State) (e : Expr) : TermElabM CollectFVars.State := do
-e ← Term.instantiateMVars e;
+e ← instantiateMVars e;
 pure $ collectFVars used e
 
 def collectUsedFVarsAtFVars (used : CollectFVars.State) (fvars : Array Expr) : TermElabM CollectFVars.State :=
 fvars.foldlM
   (fun used fvar => do
-    fvarType ← Term.inferType fvar;
+    fvarType ← inferType fvar;
     collectUsedFVars used fvarType)
   used
 
 def removeUnused (vars : Array Expr) (used : CollectFVars.State) : TermElabM (LocalContext × LocalInstances × Array Expr) := do
-localInsts ← Term.getLocalInsts;
-lctx ← Term.getLCtx;
+localInsts ← getLocalInstances;
+lctx ← getLCtx;
 (lctx, localInsts, newVars, _) ← vars.foldrM
   (fun var (result : LocalContext × LocalInstances × Array Expr × CollectFVars.State) =>
     let (lctx, localInsts, newVars, used) := result;
     if used.fvarSet.contains var.fvarId! then do
-      varType ← Term.inferType var;
+      varType ← inferType var;
       used ← Term.collectUsedFVars used varType;
       pure (lctx, localInsts, newVars.push var, used)
     else
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 296fde9217..35ef2fd912 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -510,7 +510,7 @@ fun stx => do
   withoutModifyingEnv $ runTermElabM (some `_check) $ fun _ => do
     e    ← Term.elabTerm term none;
     Term.synthesizeSyntheticMVars false;
-    type ← Term.inferType e;
+    type ← inferType e;
     logInfo (e ++ " : " ++ type);
     pure ()
 
@@ -541,9 +541,6 @@ when succeeded $
 @[builtinCommandElab «check_failure»] def elabCheckFailure : CommandElab :=
 fun stx => failIfSucceeds $ elabCheck stx
 
-def addDecl (decl : Declaration) : CommandElabM Unit := liftTermElabM none $ Term.addDecl decl
-def compileDecl (decl : Declaration) : CommandElabM Unit := liftTermElabM none $ Term.compileDecl decl
-
 def addInstance (declName : Name) : CommandElabM Unit := do
 env ← getEnv;
 env ← liftIO $ Meta.addGlobalInstance env declName;
@@ -557,11 +554,10 @@ fun stx => withoutModifyingEnv do
   ctx ← read;
   env ← getEnv;
   let addAndCompile (value : Expr) : TermElabM Unit := do {
-    type ← Term.inferType value;
+    type ← inferType value;
     let decl := Declaration.defnDecl { name := n, lparams := [], type := type,
       value := value, hints := ReducibilityHints.opaque, isUnsafe := true };
-    Term.addDecl decl;
-    Term.compileDecl decl
+    addAndCompile decl
   };
   let elabMetaEval : CommandElabM Unit := do {
     act : IO Environment ← runTermElabM (some n) fun _ => do {
@@ -570,7 +566,7 @@ fun stx => withoutModifyingEnv do
         e ← Term.withLocalDecl `env BinderInfo.default (mkConst `Lean.Environment) fun env =>
           Term.withLocalDecl `opts BinderInfo.default (mkConst `Lean.Options) fun opts => do {
             e ← Term.mkAppM `Lean.MetaHasEval.eval #[env, opts, e, toExpr false];
-            Term.mkLambda #[env, opts] e
+            mkLambdaFVars #[env, opts] e
           };
         addAndCompile e;
         env ← getEnv;
@@ -618,7 +614,7 @@ fun stx => do
   withoutModifyingEnv $ runTermElabM `_synth_cmd $ fun _ => do
     inst ← Term.elabTerm term none;
     Term.synthesizeSyntheticMVars false;
-    inst ← Term.instantiateMVars inst;
+    inst ← instantiateMVars inst;
     val  ← Term.liftMetaM $ Meta.synthInstance inst;
     logInfo val;
     pure ()
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 5f82fbf09c..a60dfddba5 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -87,9 +87,9 @@ withDeclId declId $ fun name => do
   decl ← runTermElabM declName $ fun vars => Term.elabBinders binders.getArgs $ fun xs => do {
     type ← Term.elabType typeStx;
     Term.synthesizeSyntheticMVars false;
-    type ← Term.instantiateMVars type;
-    type ← Term.mkForall xs type;
-    (type, _) ← Term.mkForallUsedOnly vars type;
+    type ← instantiateMVars type;
+    type ← mkForallFVars xs type;
+    (type, _) ← mkForallUsedOnly vars type;
     (type, _) ← Term.levelMVarToParam type;
     let usedParams  := (collectLevelParams {} type).params;
     match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams with
diff --git a/src/Lean/Elab/Definition.lean b/src/Lean/Elab/Definition.lean
index 27989cfb92..834851fdb0 100644
--- a/src/Lean/Elab/Definition.lean
+++ b/src/Lean/Elab/Definition.lean
@@ -65,18 +65,18 @@ withRef view.ref do
 Term.synthesizeSyntheticMVars;
 val     ← withRef view.val $ Term.ensureHasType type val;
 Term.synthesizeSyntheticMVars false;
-type    ← Term.instantiateMVars type;
-val     ← Term.instantiateMVars val;
+type    ← instantiateMVars type;
+val     ← instantiateMVars val;
 if view.kind.isExample then pure none
 else withUsedWhen vars xs val type view.kind.isDefOrAbbrevOrOpaque $ fun vars => do
-  type ← Term.mkForall xs type;
-  type ← Term.mkForall vars type;
-  val  ← Term.mkLambda xs val;
-  val  ← Term.mkLambda vars val;
+  type ← mkForallFVars xs type;
+  type ← mkForallFVars vars type;
+  val  ← mkLambdaFVars xs val;
+  val  ← mkLambdaFVars vars val;
   (type, nextParamIdx) ← Term.levelMVarToParam type;
   (val,  _) ← Term.levelMVarToParam val nextParamIdx;
-  type ← Term.instantiateMVars type;
-  val  ← Term.instantiateMVars val;
+  type ← instantiateMVars type;
+  val  ← instantiateMVars val;
   let shareCommonTypeVal : Std.ShareCommonM (Expr × Expr) := do {
     type ← Std.withShareCommon type;
     val  ← Std.withShareCommon val;
@@ -131,7 +131,7 @@ withDeclId view.declId $ fun name => do
     | some typeStx => do
       type ← Term.elabType typeStx;
       Term.synthesizeSyntheticMVars false;
-      type ← Term.instantiateMVars type;
+      type ← instantiateMVars type;
       withUsedWhen' vars xs type view.kind.isTheorem $ fun vars => do
         val  ← elabDefVal view.val type;
         mkDef view declName scopeLevelNames allUserLevelNames vars xs type val
diff --git a/src/Lean/Elab/DoNotation.lean b/src/Lean/Elab/DoNotation.lean
index 8d3acf95a1..9b6d80eabd 100644
--- a/src/Lean/Elab/DoNotation.lean
+++ b/src/Lean/Elab/DoNotation.lean
@@ -174,7 +174,7 @@ else do
       α  ← inferType var;
       mβ ← inferType body;
       β  ← extractTypeFormerAppArg mβ;
-      f  ← mkLambda #[var] body;
+      f  ← mkLambdaFVars #[var] body;
       -- dbgTrace (">>> f: " ++ toString f);
       let body := mkAppN bindAndInst #[α, β, action, f];
       pure body)
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 74e7c806af..eb7bd12d03 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -77,16 +77,16 @@ private partial def elabHeaderAux (views : Array InductiveView)
   if h : i < views.size then
     let view := views.get ⟨i, h⟩;
     Term.elabBinders view.binders.getArgs fun params => do
-      lctx ← Term.getLCtx;
-      localInsts ← Term.getLocalInsts;
+      lctx ← getLCtx;
+      localInsts ← getLocalInstances;
       match view.type? with
       | none         => do
-        u ← Term.mkFreshLevelMVar;
+        u ← mkFreshLevelMVar;
         let type := mkSort (mkLevelSucc u);
         elabHeaderAux (i+1) (acc.push { lctx := lctx, localInsts := localInsts, params := params, type := type, view := view })
       | some typeStx => do
         type ← Term.elabTerm typeStx none;
-        unlessM (Term.isTypeFormerType type) $
+        unlessM (isTypeFormerType type) $
           throwErrorAt typeStx "invalid inductive type, resultant type is not a sort";
         elabHeaderAux (i+1) (acc.push { lctx := lctx, localInsts := localInsts, params := params, type := type, view := view })
   else
@@ -111,7 +111,7 @@ when (views.size > 1) do
 
 private def mkTypeFor (r : ElabHeaderResult) : TermElabM Expr := do
 Term.withLocalContext r.lctx r.localInsts do
-  Term.mkForall r.params r.type
+  mkForallFVars r.params r.type
 
 private def throwUnexpectedInductiveType {α} : TermElabM α :=
 throwError "unexpected inductive resulting type"
@@ -121,14 +121,14 @@ private def getResultingType (e : Expr) : TermElabM Expr :=
 Term.liftMetaM $ Meta.forallTelescopeReducing e fun _ r => pure r
 
 private def eqvFirstTypeResult (firstType type : Expr) : MetaM Bool :=
-Meta.forallTelescopeReducing firstType fun _ firstTypeResult => Meta.isDefEq firstTypeResult type
+Meta.forallTelescopeReducing firstType fun _ firstTypeResult => isDefEq firstTypeResult type
 
 -- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
 private partial def checkParamsAndResultType (numParams : Nat) : Nat → Expr → Expr → TermElabM Unit
 | i, type, firstType => do
-  type ← Term.whnf type;
+  type ← whnf type;
   if i < numParams then do
-    firstType ← Term.whnf firstType;
+    firstType ← whnf firstType;
     match type, firstType with
     | Expr.forallE n₁ d₁ b₁ c₁, Expr.forallE n₂ d₂ b₂ c₂ => do
       unless (n₁ == n₂) $
@@ -190,7 +190,7 @@ private partial def withInductiveLocalDeclsAux {α} (namesAndTypes : Array (Name
 | i, indFVars =>
   if h : i < namesAndTypes.size then do
     let (id, type) := namesAndTypes.get ⟨i, h⟩;
-    type ← Term.liftMetaM (Meta.instantiateForall type params);
+    type ← instantiateForall type params;
     Term.withLocalDecl id BinderInfo.default type fun indFVar => withInductiveLocalDeclsAux (i+1) (indFVars.push indFVar)
   else
     x params indFVars
@@ -211,8 +211,8 @@ Term.withLocalContext r0.lctx r0.localInsts $ withRef r0.view.ref $
   withInductiveLocalDeclsAux namesAndTypes params x 0 #[]
 
 private def isInductiveFamily (indFVar : Expr) : TermElabM Bool := do
-indFVarType ← Term.inferType indFVar;
-indFVarType ← Term.whnf indFVarType;
+indFVarType ← inferType indFVar;
+indFVarType ← whnf indFVarType;
 pure !indFVarType.isSort
 
 /-
@@ -237,18 +237,18 @@ r.view.ctors.toList.mapM fun ctorView => Term.elabBinders ctorView.binders.getAr
       resultingType ← getResultingType type;
       unless (resultingType.getAppFn == indFVar) $
         throwError ("unexpected constructor resulting type" ++ indentExpr resultingType);
-      unlessM (Term.isType resultingType) $
+      unlessM (isType resultingType) $
         throwError ("unexpected constructor resulting type, type expected" ++ indentExpr resultingType);
       pure type
     };
-  type ← Term.mkForall ctorParams type;
-  type ← Term.mkForall params type;
+  type ← mkForallFVars ctorParams type;
+  type ← mkForallFVars params type;
   pure { name := ctorView.declName, type := type }
 
 /- Convert universe metavariables occurring in the `indTypes` into new parameters.
    Remark: if the resulting inductive datatype has universe metavariables, we will fix it later using
    `inferResultingUniverse`. -/
-private def levelMVarToParamAux (indTypes : List InductiveType) : StateT Nat TermElabM (List InductiveType) :=
+private def levelMVarToParamAux (indTypes : List InductiveType) : StateRefT Nat TermElabM (List InductiveType) :=
 indTypes.mapM fun indType => do
   type  ← Term.levelMVarToParam' indType.type;
   ctors ← indType.ctors.mapM fun ctor => do {
@@ -275,7 +275,7 @@ def tmpIndParam := mkLevelParam `_tmp_ind_univ_param
   Return false if `u` does not contain universe metavariables.
   Throw exception otherwise. -/
 def shouldInferResultUniverse (u : Level) : TermElabM Bool := do
-u ← Term.instantiateLevelMVars u;
+u ← instantiateLevelMVars u;
 if u.hasMVar then
   match u.getLevelOffset with
   | Level.mvar mvarId _ => do
@@ -308,7 +308,7 @@ def accLevelAtCtor : Level → Level → Nat → Array Level → Except String (
 private partial def collectUniversesFromCtorTypeAux (r : Level) (rOffset : Nat) : Nat → Expr → Array Level → TermElabM (Array Level)
 | 0,   Expr.forallE n d b c, us => do
   u ← Term.getLevel d;
-  u ← Term.instantiateLevelMVars u;
+  u ← instantiateLevelMVars u;
   match accLevelAtCtor u r rOffset us with
   | Except.error msg => throwError msg
   | Except.ok us     => Term.withLocalDecl n c.binderInfo d $ fun x =>
@@ -363,9 +363,9 @@ Term.withLCtx lctx localInsts $ k vars
 
 private def updateParams (vars : Array Expr) (indTypes : List InductiveType) : TermElabM (List InductiveType) :=
 indTypes.mapM fun indType => do
-  type ← Term.mkForall vars indType.type;
+  type ← mkForallFVars vars indType.type;
   ctors ← indType.ctors.mapM fun ctor => do {
-    ctorType ← Term.mkForall vars ctor.type;
+    ctorType ← mkForallFVars vars ctor.type;
     pure { ctor with type := ctorType }
   };
   pure { indType with type := type, ctors := ctors }
@@ -400,7 +400,7 @@ indTypes.mapM fun indType => do
         match indFVar2Const.find? e with
         | some c => some $ mkAppN c params
         | none   => none;
-      Meta.mkForall params type
+      mkForallFVars params type
     };
     pure { ctor with type := type }
   };
@@ -439,7 +439,7 @@ adaptReader (fun (ctx : Term.Context) => { ctx with levelNames := allUserLevelNa
       (fun i (indTypes : List InductiveType) => do
         let indFVar := indFVars.get! i;
         let r       := rs.get! i;
-        type  ← Term.mkForall params r.type;
+        type  ← mkForallFVars params r.type;
         ctors ← elabCtors indFVar params r;
         let indType := { name := r.view.declName, type := type, ctors := ctors : InductiveType };
         pure (indType :: indTypes))
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 3169100e67..017de366b9 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -174,7 +174,7 @@ private def getNumExplicitCtorParams (ctorVal : ConstructorVal) : TermElabM Nat
 liftMetaM $ Meta.forallBoundedTelescope ctorVal.type ctorVal.nparams fun ps _ =>
   ps.foldlM
     (fun acc p => do
-      localDecl ← Meta.getLocalDecl p.fvarId!;
+      localDecl ← getLocalDecl p.fvarId!;
       if localDecl.binderInfo.isExplicit then pure $ acc+1 else pure acc)
     0
 
@@ -377,7 +377,7 @@ patternVarDecls.foldlM
     match pdecl with
     | PatternVarDecl.localVar fvarId => do
       decl ← getLocalDecl fvarId;
-      decl ← liftMetaM $ Meta.instantiateLocalDeclMVars decl;
+      decl ← instantiateLocalDeclMVars decl;
       pure $ decls.push decl
     | PatternVarDecl.anonymousVar mvarId fvarId => do
       e ← instantiateMVars (mkMVar mvarId);
@@ -389,7 +389,7 @@ patternVarDecls.foldlM
         assignExprMVar newMVarId (mkFVar fvarId);
         trace `Elab.match fun _ => "finalizePatternDecls: " ++ mkMVar newMVarId ++ " := " ++ mkFVar fvarId;
         decl ← getLocalDecl fvarId;
-        decl ← liftMetaM $ Meta.instantiateLocalDeclMVars decl;
+        decl ← instantiateLocalDeclMVars decl;
         pure $ decls.push decl
       | _ => pure decls)
   #[]
@@ -427,15 +427,15 @@ private def getFieldsBinderInfoAux (ctorVal : ConstructorVal) : Nat → Expr →
 private def mkLocalDeclFor (mvar : Expr) : M Pattern := do
 let mvarId := mvar.mvarId!;
 s ← get;
-val? ← liftM $ liftMetaM $ Meta.getExprMVarAssignment? mvarId;
+val? ← getExprMVarAssignment? mvarId;
 match val? with
 | some val => pure $ Pattern.inaccessible val
 | none => do
   fvarId ← mkFreshId;
-  type   ← liftM $ inferType mvar;
+  type   ← inferType mvar;
   /- HACK: `fvarId` is not in the scope of `mvarId`
      If this generates problems in the future, we should update the metavariable declarations. -/
-  liftM $ assignExprMVar mvarId (mkFVar fvarId);
+  assignExprMVar mvarId (mkFVar fvarId);
   let userName := (`_x).appendIndexAfter (s.localDecls.size+1);
   let newDecl := LocalDecl.cdecl (arbitrary _) fvarId userName type BinderInfo.default;
   modify $ fun s =>
@@ -492,7 +492,7 @@ partial def main : Expr → M Pattern
   else if e.isMVar then do
     mkLocalDeclFor e
   else do
-    newE ← liftM $ whnf e;
+    newE ← whnf e;
     if newE != e then
       main newE
     else match e.getAppFn with
@@ -520,7 +520,7 @@ end ToDepElimPattern
 
 def withDepElimPatterns {α} (localDecls : Array LocalDecl) (ps : Array Expr) (k : Array LocalDecl → Array Pattern → TermElabM α) : TermElabM α := do
 (patterns, s) ← (ps.mapM ToDepElimPattern.main).run { localDecls := localDecls };
-localDecls ← s.localDecls.mapM fun d => liftMetaM $ Meta.instantiateLocalDeclMVars d;
+localDecls ← s.localDecls.mapM fun d => instantiateLocalDeclMVars d;
 /- toDepElimPatterns may have added new localDecls. Thus, we must update the local context before we execute `k` -/
 lctx ← getLCtx;
 let lctx := localDecls.foldl (fun (lctx : LocalContext) d => lctx.erase d.fvarId) lctx;
@@ -543,7 +543,7 @@ withPatternVars patternVars fun patternVarDecls => do
   withElaboratedLHS patternVarDecls alt.patterns matchType fun altLHS matchType => do
     rhs ← elabTermEnsuringType alt.rhs matchType;
     let xs := altLHS.fvarDecls.toArray.map LocalDecl.toExpr;
-    rhs ← if xs.isEmpty then pure $ mkThunk rhs else mkLambda xs rhs;
+    rhs ← if xs.isEmpty then pure $ mkThunk rhs else mkLambdaFVars xs rhs;
     trace `Elab.match fun _ => "rhs: " ++ rhs;
     -- TODO: check whether altLHS still has metavariables
     pure (altLHS, rhs)
@@ -551,7 +551,7 @@ withPatternVars patternVars fun patternVarDecls => do
 def mkMotiveType (matchType : Expr) (expectedType : Expr) : TermElabM Expr := do
 liftMetaM $ Meta.forallTelescopeReducing matchType fun xs matchType => do
   u ← Meta.getLevel matchType;
-  Meta.mkForall xs (mkSort u)
+  mkForallFVars xs (mkSort u)
 
 def mkElim (elimName : Name) (motiveType : Expr) (lhss : List AltLHS) : TermElabM ElimResult :=
 liftMetaM $ Meta.Match.mkElim elimName motiveType lhss
@@ -573,7 +573,7 @@ alts ← matchAlts.mapM $ fun alt => elabMatchAltView alt matchType;
 let rhss := alts.map Prod.snd;
 let altLHSS := alts.map Prod.fst;
 motiveType ← mkMotiveType matchType expectedType;
-motive ← liftMetaM $ Meta.forallTelescopeReducing matchType fun xs matchType => Meta.mkLambda xs matchType;
+motive ← liftMetaM $ Meta.forallTelescopeReducing matchType fun xs matchType => mkLambdaFVars xs matchType;
 elimName ← mkAuxName `elim;
 elimResult ← mkElim elimName motiveType altLHSS.toList;
 reportElimResultErrors elimResult;
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index b8f87fe41b..f782b4b470 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -646,9 +646,9 @@ else match e.getAppFn with
 
 /-- Reduce default value. It performs beta reduction and projections of the given structures. -/
 partial def reduce (structNames : Array Name) : Expr → MetaM Expr
-| e@(Expr.lam _ _ _ _)     => Meta.lambdaTelescope e $ fun xs b => do b ← reduce b; Meta.mkLambda xs b
-| e@(Expr.forallE _ _ _ _) => Meta.forallTelescope e $ fun xs b => do b ← reduce b; Meta.mkForall xs b
-| e@(Expr.letE _ _ _ _ _)  => Meta.lambdaTelescope e $ fun xs b => do b ← reduce b; Meta.mkLambda xs b
+| e@(Expr.lam _ _ _ _)     => Meta.lambdaTelescope e $ fun xs b => do b ← reduce b; mkLambdaFVars xs b
+| e@(Expr.forallE _ _ _ _) => Meta.forallTelescope e $ fun xs b => do b ← reduce b; mkForallFVars xs b
+| e@(Expr.letE _ _ _ _ _)  => Meta.lambdaTelescope e $ fun xs b => do b ← reduce b; mkLetFVars xs b
 | e@(Expr.proj _ i b _)    => do
   r? ← Meta.reduceProj? b i;
   match r? with
@@ -674,7 +674,7 @@ partial def reduce (structNames : Array Name) : Expr → MetaM Expr
   else
     pure $ e.updateMData! b
 | e@(Expr.mvar mvarId _) => do
-  val? ← Meta.getExprMVarAssignment? mvarId;
+  val? ← getExprMVarAssignment? mvarId;
   match val? with
   | some val => if val.isMVar then reduce val else pure val
   | none     => pure e
@@ -728,7 +728,7 @@ partial def step : Struct → M Unit
 
 partial def propagateLoop (hierarchyDepth : Nat) : Nat → Struct → M Unit
 | d, struct => do
-  mctx ← liftM $ getMCtx;
+  mctx ← getMCtx;
   match findDefaultMissing? mctx struct with
   | none       => pure () -- Done
   | some field =>
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 33fb3b743e..90674f5a3f 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -217,7 +217,7 @@ private partial def processSubfields {α} (structDeclName : Name) (parentFVar :
     when (containsFieldName infos subfieldName) $
       throwError ("field '" ++ subfieldName ++ "' from '" ++ parentStructName ++ "' has already been declared");
     val  ← Term.liftMetaM $ Meta.mkProjection parentFVar subfieldName;
-    type ← Term.inferType val;
+    type ← inferType val;
     Term.withLetDecl subfieldName type val fun subfieldFVar =>
       /- The following `declName` is only used for creating the `_default` auxiliary declaration name when
          its default value is overwritten in the structure. -/
@@ -253,7 +253,7 @@ match view.type? with
   | none        => pure (none, none)
   | some valStx => do
     value ← Term.elabTerm valStx none;
-    value ← Term.mkLambda params value;
+    value ← mkLambdaFVars params value;
     pure (none, value)
 | some typeStx => do
   type ← Term.elabType typeStx;
@@ -261,8 +261,8 @@ match view.type? with
   | none        => pure (type, none)
   | some valStx => do
     value ← Term.elabTermEnsuringType valStx type;
-    type  ← Term.mkForall params type;
-    value ← Term.mkLambda params value;
+    type  ← mkForallFVars params type;
+    value ← mkLambdaFVars params value;
     pure (type, value)
 
 private partial def withFields {α} (views : Array StructFieldView) : Nat → Array StructFieldInfo → (Array StructFieldInfo → TermElabM α) → TermElabM α
@@ -281,7 +281,7 @@ private partial def withFields {α} (views : Array StructFieldView) : Nat → Ar
                                     kind := StructFieldKind.newField, inferMod := view.inferMod };
           withFields (i+1) infos k
       | none, some value => do
-        type ← Term.inferType value;
+        type ← inferType value;
         Term.withLocalDecl view.name view.binderInfo type $ fun fieldFVar =>
           let infos := infos.push { name := view.name, declName := view.declName, fvar := fieldFVar, kind := StructFieldKind.newField, inferMod := view.inferMod };
           withFields (i+1) infos k
@@ -294,7 +294,7 @@ private partial def withFields {α} (views : Array StructFieldView) : Nat → Ar
         | some valStx => do
           when (!view.binders.getArgs.isEmpty || view.type?.isSome) $
             throwErrorAt view.type?.get! ("omit field '" ++ view.name ++ "' type to set default value");
-          fvarType ← Term.inferType info.fvar;
+          fvarType ← inferType info.fvar;
           value ← Term.elabTermEnsuringType valStx fvarType;
           let infos := infos.push { info with value? := value };
           withFields (i+1) infos k
@@ -303,7 +303,7 @@ private partial def withFields {α} (views : Array StructFieldView) : Nat → Ar
     k infos
 
 private def getResultUniverse (type : Expr) : TermElabM Level := do
-type ← Term.whnf type;
+type ← whnf type;
 match type with
 | Expr.sort u _ => pure u
 | _             => throwError "unexpected structure resulting type"
@@ -312,12 +312,12 @@ private def removeUnused (scopeVars : Array Expr) (params : Array Expr) (fieldIn
     : TermElabM (LocalContext × LocalInstances × Array Expr) := do
 used ← params.foldlM
    (fun (used : CollectFVars.State) p => do
-     type ← Term.inferType p;
+     type ← inferType p;
      Term.collectUsedFVars used type)
    {};
 used ← fieldInfos.foldlM
   (fun (used : CollectFVars.State) info => do
-    fvarType ← Term.inferType info.fvar;
+    fvarType ← inferType info.fvar;
     used ← Term.collectUsedFVars used fvarType;
     match info.value? with
     | none       => pure used
@@ -330,16 +330,16 @@ private def withUsed {α} (scopeVars : Array Expr) (params : Array Expr) (fieldI
 (lctx, localInsts, vars) ← removeUnused scopeVars params fieldInfos;
 Term.withLCtx lctx localInsts $ k vars
 
-private def levelMVarToParamFVar (fvar : Expr) : StateT Nat TermElabM Unit := do
-type ← liftM $ Term.inferType fvar;
+private def levelMVarToParamFVar (fvar : Expr) : StateRefT Nat TermElabM Unit := do
+type ← inferType fvar;
 _ ← Term.levelMVarToParam' type;
 pure ()
 
-private def levelMVarToParamFVars (fvars : Array Expr) : StateT Nat TermElabM Unit :=
+private def levelMVarToParamFVars (fvars : Array Expr) : StateRefT Nat TermElabM Unit :=
 fvars.forM levelMVarToParamFVar
 
 private def levelMVarToParamAux (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo)
-    : StateT Nat TermElabM (Array StructFieldInfo) := do
+    : StateRefT Nat TermElabM (Array StructFieldInfo) := do
 levelMVarToParamFVars scopeVars;
 levelMVarToParamFVars params;
 fieldInfos.mapM fun info => do
@@ -356,9 +356,9 @@ private def levelMVarToParam (scopeVars : Array Expr) (params : Array Expr) (fie
 private partial def collectUniversesFromFields (r : Level) (rOffset : Nat) (fieldInfos : Array StructFieldInfo) : TermElabM (Array Level) := do
 fieldInfos.foldlM
   (fun (us : Array Level) (info : StructFieldInfo) => do
-    type ← Term.inferType info.fvar;
+    type ← inferType info.fvar;
     u ← Term.getLevel type;
-    u ← Term.instantiateLevelMVars u;
+    u ← instantiateLevelMVars u;
     match accLevelAtCtor u r rOffset us with
     | Except.error msg => throwError msg
     | Except.ok us     => pure us)
@@ -372,13 +372,13 @@ match r with
 | Level.mvar mvarId _ => do
   us ← collectUniversesFromFields r rOffset fieldInfos;
   let rNew := Level.mkNaryMax us.toList;
-  Term.assignLevelMVar mvarId rNew;
-  Term.instantiateMVars type
+  assignLevelMVar mvarId rNew;
+  instantiateMVars type
 | _ => throwError "failed to compute resulting universe level of structure, provide universe explicitly"
 
 private def collectLevelParamsInFVar (s : CollectLevelParams.State) (fvar : Expr) : TermElabM CollectLevelParams.State := do
-type ← Term.inferType fvar;
-type ← Term.instantiateMVars type;
+type ← inferType fvar;
+type ← instantiateMVars type;
 pure $ collectLevelParams s type
 
 private def collectLevelParamsInFVars (fvars : Array Expr) (s : CollectLevelParams.State) : TermElabM CollectLevelParams.State :=
@@ -395,7 +395,7 @@ private def addCtorFields (fieldInfos : Array StructFieldInfo) : Nat → Expr 
 | i+1, type => do
   let info := fieldInfos.get! i;
   decl ← Term.getFVarLocalDecl! info.fvar;
-  type ← Term.instantiateMVars type;
+  type ← instantiateMVars type;
   let type := type.abstract #[info.fvar];
   match info.kind with
   | StructFieldKind.fromParent =>
@@ -411,8 +411,8 @@ private def mkCtor (view : StructView) (levelParams : List Name) (params : Array
 withRef view.ref do
 let type := mkAppN (mkConst view.declName (levelParams.map mkLevelParam)) params;
 type ← addCtorFields fieldInfos fieldInfos.size type;
-type ← Term.mkForall params type;
-type ← Term.instantiateMVars type;
+type ← mkForallFVars params type;
+type ← instantiateMVars type;
 let type := type.inferImplicit params.size !view.ctor.inferMod;
 pure { name := view.ctor.declName, type := type }
 
@@ -436,8 +436,8 @@ withFields view.fields 0 fieldInfos fun fieldInfos => do
     | Except.ok levelParams => do
       let params := scopeVars ++ view.params;
       ctor ← mkCtor view levelParams params fieldInfos;
-      type ← Term.mkForall params type;
-      type ← Term.instantiateMVars type;
+      type ← mkForallFVars params type;
+      type ← instantiateMVars type;
       let indType := { name := view.declName, type := type, ctors := [ctor] : InductiveType };
       let decl    := Declaration.inductDecl levelParams params.size [indType] view.modifiers.isUnsafe;
       let projInfos := (fieldInfos.filter fun (info : StructFieldInfo) => !info.isFromParent).toList.map fun (info : StructFieldInfo) =>
@@ -447,12 +447,12 @@ withFields view.fields 0 fieldInfos fun fieldInfos => do
         pure (info.isSubobject && decl.binderInfo.isInstImplicit)
       };
       let projInstances := instParents.toList.map fun info => info.declName;
-      mctx ← Term.getMCtx;
-      lctx ← Term.getLCtx;
-      localInsts ← Term.getLocalInsts;
+      mctx ← getMCtx;
+      lctx ← getLCtx;
+      localInsts ← getLocalInstances;
       let fieldsWithDefault := fieldInfos.filter fun info => info.value?.isSome;
       defaultAuxDecls ← fieldsWithDefault.mapM fun info => do {
-        type ← Term.inferType info.fvar;
+        type ← inferType info.fvar;
         pure (info.declName ++ `_default, type, info.value?.get!)
       };
       /- The `mctx`, `lctx`, `localInsts` and `defaultAuxDecls` are used to create the auxiliary `_default` declarations *after* the structure has been declarated.
@@ -490,12 +490,12 @@ when (hasUnit && hasEq && hasHEq) $ modifyEnv fun env => mkNoConfusion env declN
 private def addDefaults (mctx : MetavarContext) (lctx : LocalContext) (localInsts : LocalInstances)
     (defaultAuxDecls : Array (Name × Expr × Expr)) : CommandElabM Unit :=
 liftTermElabM none $ Term.withLocalContext lctx localInsts do
-  Term.setMCtx mctx;
+  setMCtx mctx;
   defaultAuxDecls.forM fun ⟨declName, type, value⟩ => do
     /- The identity function is used as "marker". -/
     value ← Term.liftMetaM $ Meta.mkId value;
     let zeta := true; -- expand `let-declarations`
-    _ ← Term.mkAuxDefinition declName type value zeta;
+    _ ← mkAuxDefinition declName type value zeta;
     modifyEnv fun env => setReducibilityStatus env declName ReducibilityStatus.reducible;
     pure ()
 
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 9c90c2f0f4..1b530b9ff9 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -41,15 +41,6 @@ structure BacktrackableState :=
 abbrev TacticM := ReaderT Context $ StateRefT State $ TermElabM
 abbrev Tactic  := Syntax → TacticM Unit
 
-def getMCtx : TacticM MetavarContext := do s ← getThe Meta.State; pure s.mctx
-def getLCtx : TacticM LocalContext := do ctx ← readThe Meta.Context; pure ctx.lctx
-def getLocalInsts : TacticM LocalInstances := do ctx ← readThe Meta.Context; pure ctx.localInstances
-def getMVarDecl (mvarId : MVarId) : TacticM MetavarDecl := do mctx ← getMCtx; pure $ mctx.getDecl mvarId
-
-def setMCtx (mctx : MetavarContext) : TacticM Unit := modifyThe Meta.State fun s => { s with mctx := mctx }
-
-@[inline] def modifyMCtx (f : MetavarContext → MetavarContext) : TacticM Unit := modifyThe Meta.State $ fun s => { s with mctx := f s.mctx }
-
 def saveBacktrackableState : TacticM BacktrackableState := do
 env ← getEnv;
 mctx ← getMCtx;
@@ -98,15 +89,8 @@ liftM x
 @[inline] def liftMetaM {α} (x : MetaM α) : TacticM α :=
 liftTermElabM $ Term.liftMetaM x
 
-def instantiateMVars (e : Expr) : TacticM Expr := liftTermElabM $ Term.instantiateMVars e
-def isExprMVarAssigned (mvarId : MVarId) : TacticM Bool := liftTermElabM $ Term.isExprMVarAssigned mvarId
-def assignExprMVar (mvarId : MVarId) (val : Expr) : TacticM Unit := liftTermElabM $ Term.assignExprMVar mvarId val
 def ensureHasType (expectedType? : Option Expr) (e : Expr) : TacticM Expr := liftTermElabM $ Term.ensureHasType expectedType? e
 def reportUnsolvedGoals (goals : List MVarId) : TacticM Unit := liftTermElabM $ Term.reportUnsolvedGoals goals
-def inferType (e : Expr) : TacticM Expr := liftTermElabM $ Term.inferType e
-def whnf (e : Expr) : TacticM Expr := liftTermElabM $ Term.whnf e
-def whnfCore (e : Expr) : TacticM Expr := liftTermElabM $ Term.whnfCore e
-def unfoldDefinition? (e : Expr) : TacticM (Option Expr) := liftTermElabM $ Term.unfoldDefinition? e
 def resolveGlobalName (n : Name) : TacticM (List (Name × List String)) := liftTermElabM $ Term.resolveGlobalName n
 
 /-- Collect unassigned metavariables -/
@@ -233,7 +217,7 @@ if b then resettingSynthInstanceCache x else x
 
 def withMVarContext {α} (mvarId : MVarId) (x : TacticM α) : TacticM α := do
 mvarDecl   ← getMVarDecl mvarId;
-localInsts ← getLocalInsts;
+localInsts ← getLocalInstances;
 let needReset := localInsts == mvarDecl.localInstances;
 withLCtx mvarDecl.lctx mvarDecl.localInstances $ resettingSynthInstanceCacheWhen needReset x
 
@@ -353,7 +337,7 @@ private def getIntrosSize : Expr → Nat
 fun stx => match_syntax stx with
   | `(tactic| intros)       => liftMetaTactic $ fun mvarId => do
     type ← Meta.getMVarType mvarId;
-    type ← Meta.instantiateMVars type;
+    type ← instantiateMVars type;
     let n := getIntrosSize type;
     (_, mvarId) ← Meta.introN mvarId n;
     pure [mvarId]
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index da9b272562..fc2ac34410 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -18,7 +18,7 @@ def elabTerm (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false)
 withRef stx $ liftTermElabM $ adaptReader (fun (ctx : Term.Context) => { ctx with errToSorry := false }) $ do
   e ← Term.elabTerm stx expectedType?;
   Term.synthesizeSyntheticMVars mayPostpone;
-  Term.instantiateMVars e
+  instantiateMVars e
 
 @[builtinTactic «exact»] def evalExact : Tactic :=
 fun stx => match_syntax stx with
diff --git a/src/Lean/Elab/Tactic/Generalize.lean b/src/Lean/Elab/Tactic/Generalize.lean
index f0090979ea..500c703671 100644
--- a/src/Lean/Elab/Tactic/Generalize.lean
+++ b/src/Lean/Elab/Tactic/Generalize.lean
@@ -21,12 +21,12 @@ stx.getIdAt 4
 
 private def evalGeneralizeFinalize (mvarId : MVarId) (e : Expr) (target : Expr) : MetaM (List MVarId) := do
 tag         ← Meta.getMVarTag mvarId;
-eType       ← Meta.inferType e;
+eType       ← inferType e;
 u           ← Meta.getLevel eType;
 mvar' ← Meta.mkFreshExprSyntheticOpaqueMVar target tag;
 let rfl    := mkApp2 (Lean.mkConst `Eq.refl [u]) eType e;
 let val    := mkApp2 mvar' e rfl;
-Meta.assignExprMVar mvarId val;
+assignExprMVar mvarId val;
 let mvarId' := mvar'.mvarId!;
 (_, mvarId') ← Meta.introN mvarId' 2 [] false;
 pure [mvarId']
@@ -34,11 +34,11 @@ pure [mvarId']
 private def evalGeneralizeWithEq (h : Name) (e : Expr) (x : Name) : TacticM Unit :=
 liftMetaTactic $ fun mvarId => do
   mvarId      ← Meta.generalize mvarId e x;
-  mvarDecl    ← Meta.getMVarDecl mvarId;
+  mvarDecl    ← getMVarDecl mvarId;
   match mvarDecl.type with
   | Expr.forallE _ _ b _ => do
     (_, mvarId) ← Meta.intro1 mvarId false;
-    eType       ← Meta.inferType e;
+    eType       ← inferType e;
     u           ← Meta.getLevel eType;
     let eq     := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0);
     let target := Lean.mkForall x BinderInfo.default eType $ Lean.mkForall h BinderInfo.default eq (b.liftLooseBVars 0 1);
@@ -48,7 +48,7 @@ liftMetaTactic $ fun mvarId => do
 -- If generalizing fails, fall back to not replacing anything
 private def evalGeneralizeFallback (h : Name) (e : Expr) (x : Name) : TacticM Unit :=
 liftMetaTactic $ fun mvarId => do
-  eType       ← Meta.inferType e;
+  eType       ← inferType e;
   u           ← Meta.getLevel eType;
   mvarType    ← Meta.getMVarType mvarId;
   let eq     := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0);
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 7fbc44d497..80c04de41e 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -104,8 +104,8 @@ structure RecInfo :=
 
 def getInductiveValFromMajor (major : Expr) : TacticM InductiveVal :=
 liftMetaMAtMain $ fun mvarId => do
-  majorType ← Meta.inferType major;
-  majorType ← Meta.whnf majorType;
+  majorType ← inferType major;
+  majorType ← whnf majorType;
   match majorType.getAppFn with
   | Expr.const n _ _ => do
     env ← getEnv;
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index bbbf313ddd..c9a73bd166 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -145,17 +145,17 @@ newTraceState ← getTraceState;
 saveTraceAsMessages newTraceState;
 setTraceState oldTraceState
 
-@[inline] def liftMetaM {α} (x : MetaM α) : TermElabM α := do
+@[inline] protected def liftMetaM {α} (x : MetaM α) : TermElabM α := do
 oldTraceState ← getTraceState;
 setTraceState {};
 finally (liftMetaMCore x) (liftMetaMFinalizer oldTraceState)
 
 @[inline] def liftCoreM {α} (x : CoreM α) : TermElabM α :=
-liftMetaM $ liftM x
+Term.liftMetaM $ liftM x
+
+instance : MonadMetaM TermElabM :=
+{ liftMetaM := fun α => Term.liftMetaM }
 
-def getMCtx : TermElabM MetavarContext := do s ← getThe Meta.State; pure s.mctx
-def getLCtx : TermElabM LocalContext := do ctx ← readThe Meta.Context; pure ctx.lctx
-def getLocalInsts : TermElabM LocalInstances := do ctx ← readThe Meta.Context; pure ctx.localInstances
 def getLevelNames : TermElabM (List Name) := do ctx ← read; pure ctx.levelNames
 def getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl := do
   lctx ← getLCtx;
@@ -164,8 +164,6 @@ def getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl := do
   | none   => unreachable!
 def getMessageLog : TermElabM MessageLog := do s ← get; pure s.messages
 
-def setMCtx (mctx : MetavarContext) : TermElabM Unit := modifyThe Meta.State $ fun s => { s with mctx := mctx }
-
 private def addContext' (msg : MessageData) : TermElabM MessageData := do
 env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
 pure (MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msg)
@@ -222,7 +220,6 @@ def getCurrNamespace : TermElabM Name := do ctx ← read; pure ctx.currNamespace
 def getOpenDecls : TermElabM (List OpenDecl) := do ctx ← read; pure ctx.openDecls
 def isExprMVarAssigned (mvarId : MVarId) : TermElabM Bool := do mctx ← getMCtx; pure $ mctx.isExprAssigned mvarId
 def getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl := do mctx ← getMCtx; pure $ mctx.getDecl mvarId
-def assignExprMVar (mvarId : MVarId) (val : Expr) : TermElabM Unit := modifyThe Meta.State $ fun s => { s with mctx := s.mctx.assignExpr mvarId val }
 def assignLevelMVar (mvarId : MVarId) (val : Level) : TermElabM Unit := modifyThe Meta.State $ fun s => { s with mctx := s.mctx.assignLevel mvarId val }
 
 def logTrace (cls : Name) (msg : MessageData) : TermElabM Unit := do
@@ -254,38 +251,22 @@ def dbgTrace {α} [HasToString α] (a : α) : TermElabM Unit :=
 _root_.dbgTrace (toString a) $ fun _ => pure ()
 
 def ppGoal (mvarId : MVarId) : TermElabM Format := liftMetaM $ Meta.ppGoal mvarId
-def isType (e : Expr) : TermElabM Bool := liftMetaM $ Meta.isType e
-def isTypeFormer (e : Expr) : TermElabM Bool := liftMetaM $ Meta.isTypeFormer e
-def isTypeFormerType (e : Expr) : TermElabM Bool := liftMetaM $ Meta.isTypeFormerType e
-def isDefEqNoConstantApprox (t s : Expr) : TermElabM Bool := liftMetaM $ Meta.approxDefEq $ Meta.isDefEq t s
-def isDefEq (t s : Expr) : TermElabM Bool := liftMetaM $ Meta.fullApproxDefEq $ Meta.isDefEq t s
-def isLevelDefEq (u v : Level) : TermElabM Bool := liftMetaM $ Meta.isLevelDefEq u v
-def inferType (e : Expr) : TermElabM Expr := liftMetaM $ Meta.inferType e
-def whnf (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnf e
-def whnfForall (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnfForall e
-def whnfCore (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnfCore e
-def unfoldDefinition? (e : Expr) : TermElabM (Option Expr) := liftMetaM $ Meta.unfoldDefinition? e
-def instantiateMVars (e : Expr) : TermElabM Expr := liftMetaM $ Meta.instantiateMVars e
-def instantiateLevelMVars (u : Level) : TermElabM Level := liftMetaM $ Meta.instantiateLevelMVars u
+def isDefEqNoConstantApprox (t s : Expr) : TermElabM Bool := liftMetaM $ Meta.approxDefEq $ Lean.isDefEq t s
+def isDefEq (t s : Expr) : TermElabM Bool := liftMetaM $ Meta.fullApproxDefEq $ Lean.isDefEq t s
 def isClass? (t : Expr) : TermElabM (Option Name) := liftMetaM $ Meta.isClass? t
-def mkFreshLevelMVar : TermElabM Level := liftMetaM $ Meta.mkFreshLevelMVar
 def mkFreshExprMVar (type? : Option Expr := none) (kind : MetavarKind := MetavarKind.natural) (userName? : Name := Name.anonymous) : TermElabM Expr :=
 match type? with
-| some type => liftMetaM $ Meta.mkFreshExprMVar type userName? kind
-| none      => liftMetaM $ do u ← Meta.mkFreshLevelMVar; type ← Meta.mkFreshExprMVar (mkSort u); Meta.mkFreshExprMVar type userName? kind
+| some type => liftMetaM $ Lean.mkFreshExprMVar type userName? kind
+| none      => liftMetaM $ do u ← mkFreshLevelMVar; type ← Lean.mkFreshExprMVar (mkSort u); Lean.mkFreshExprMVar type userName? kind
 def mkFreshExprMVarWithId (mvarId : MVarId) (type? : Option Expr := none) (kind : MetavarKind := MetavarKind.natural) (userName? : Name := Name.anonymous)
     : TermElabM Expr :=
 match type? with
-| some type => liftMetaM $ Meta.mkFreshExprMVarWithId mvarId type userName? kind
-| none      => liftMetaM $ do u ← Meta.mkFreshLevelMVar; type ← Meta.mkFreshExprMVar (mkSort u); Meta.mkFreshExprMVarWithId mvarId type userName? kind
+| some type => liftMetaM $ Lean.mkFreshExprMVarWithId mvarId type userName? kind
+| none      => liftMetaM $ do u ← Lean.mkFreshLevelMVar; type ← Lean.mkFreshExprMVar (mkSort u); Lean.mkFreshExprMVarWithId mvarId type userName? kind
 def mkFreshTypeMVar (kind : MetavarKind := MetavarKind.natural) (userName? : Name := Name.anonymous) : TermElabM Expr :=
-liftMetaM $ do u ← Meta.mkFreshLevelMVar; Meta.mkFreshExprMVar (mkSort u) userName? kind
+liftMetaM $ do u ← Lean.mkFreshLevelMVar; Lean.mkFreshExprMVar (mkSort u) userName? kind
+
 def getLevel (type : Expr) : TermElabM Level := liftMetaM $ Meta.getLevel type
-def getLocalDecl (fvarId : FVarId) : TermElabM LocalDecl := liftMetaM $ Meta.getLocalDecl fvarId
-def mkForall (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM $ Meta.mkForall xs e
-def mkForallUsedOnly (xs : Array Expr) (e : Expr) : TermElabM (Expr × Nat) := liftMetaM $ Meta.mkForallUsedOnly xs e
-def mkLambda (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM $ Meta.mkLambda xs e
-def mkLet (x : Expr) (e : Expr) : TermElabM Expr := mkLambda #[x] e
 def trySynthInstance (type : Expr) : TermElabM (LOption Expr) := liftMetaM $ Meta.trySynthInstance type
 def mkAppM (constName : Name) (args : Array Expr) : TermElabM Expr := liftMetaM $ Meta.mkAppM constName args
 def mkExpectedTypeHint (e : Expr) (expectedType : Expr) : TermElabM Expr := liftMetaM $ Meta.mkExpectedTypeHint e expectedType
@@ -368,7 +349,7 @@ setMCtx r.mctx;
 pure (r.expr, r.nextParamIdx)
 
 /-- Variant of `levelMVarToParam` where `nextParamIdx` is stored in a state monad. -/
-def levelMVarToParam' (e : Expr) : StateT Nat TermElabM Expr := do
+def levelMVarToParam' (e : Expr) : StateRefT Nat TermElabM Expr := do
 nextParamIdx ← get;
 (e, nextParamIdx) ← liftM $ levelMVarToParam e nextParamIdx;
 set nextParamIdx;
@@ -440,7 +421,7 @@ else
 def withLocalDecl {α} (n : Name) (binderInfo : BinderInfo) (type : Expr) (k : Expr → TermElabM α) : TermElabM α := do
 fvarId     ← mkFreshFVarId;
 lctx       ← getLCtx;
-localInsts ← getLocalInsts;
+localInsts ← getLocalInstances;
 let lctx   := lctx.mkLocalDecl fvarId n type binderInfo;
 let fvar   := mkFVar fvarId;
 c?         ← isClass? type;
@@ -453,7 +434,7 @@ match c? with
 def withLetDecl {α} (n : Name) (type : Expr) (val : Expr) (k : Expr → TermElabM α) : TermElabM α := do
 fvarId     ← mkFreshFVarId;
 lctx       ← getLCtx;
-localInsts ← getLocalInsts;
+localInsts ← getLocalInstances;
 let lctx   := lctx.mkLetDecl fvarId n type val;
 let fvar   := mkFVar fvarId;
 c?         ← isClass? type;
@@ -865,7 +846,7 @@ else match expectedType? with
 def elabImplicitLambdaAux (stx : Syntax) (catchExPostpone : Bool) (expectedType : Expr) (fvars : Array Expr) : TermElabM Expr := do
 body ← elabUsingElabFns stx expectedType catchExPostpone;
 -- body ← ensureHasType stx expectedType body;
-r ← mkLambda fvars body;
+r ← mkLambdaFVars fvars body;
 trace `Elab.implicitForall $ fun _ => r;
 pure r
 
@@ -947,7 +928,7 @@ finally x (restoreSynthInstanceCache savedSythInstance)
 if b then resettingSynthInstanceCache x else x
 
 def withLocalContext {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : TermElabM α) : TermElabM α := do
-localInstsCurr ← getLocalInsts;
+localInstsCurr ← getLocalInstances;
 adaptTheReader Meta.Context (fun ctx => { ctx with lctx := lctx, localInstances := localInsts }) $
   if localInsts == localInstsCurr then
     x
@@ -960,7 +941,7 @@ adaptTheReader Meta.Context (fun ctx => { ctx with lctx := lctx, localInstances
   different from the current ones. -/
 def withMVarContext {α} (mvarId : MVarId) (x : TermElabM α) : TermElabM α := do
 mvarDecl   ← getMVarDecl mvarId;
-localInsts ← getLocalInsts;
+localInsts ← getLocalInstances;
 let needReset := localInsts == mvarDecl.localInstances;
 withLCtx mvarDecl.lctx mvarDecl.localInstances $ resettingSynthInstanceCacheWhen needReset x
 
@@ -1012,31 +993,6 @@ u ← mkFreshLevelMVar;
 type ← elabTerm stx (mkSort u);
 withRef stx $ ensureType type
 
-def addDecl (decl : Declaration) : TermElabM Unit := do
-env ← getEnv;
-match env.addDecl decl with
-| Except.ok    env => setEnv env
-| Except.error kex => do opts ← getOptions; throwError (kex.toMessageData opts)
-
-def compileDecl (decl : Declaration) : TermElabM Unit := do
-env  ← getEnv;
-opts ← getOptions;
-match env.compileDecl opts decl with
-| Except.ok env    => setEnv env
-| Except.error kex => throwError (kex.toMessageData opts)
-
-def mkAuxDefinition (declName : Name) (type : Expr) (value : Expr) (zeta : Bool := false) : TermElabM Expr := do
-env ← getEnv;
-opts ← getOptions;
-mctx ← getMCtx;
-lctx ← getLCtx;
-match Lean.mkAuxDefinition env opts mctx lctx declName type value zeta with
-| Except.error ex          => throwError (ex.toMessageData opts)
-| Except.ok (r, env, mctx) => do
-  setEnv env;
-  setMCtx mctx;
-  pure r
-
 private partial def mkAuxNameAux (env : Environment) (base : Name) : Nat → Name
 | i =>
   let candidate := base.appendIndexAfter i;
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 43ac64bdf6..20486935a4 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -144,20 +144,41 @@ instance hasEval {α} [MetaHasEval α] : MetaHasEval (MetaM α) :=
 protected def throwIsDefEqStuck {α} : MetaM α :=
 throw $ Exception.internal isDefEqStuckExceptionId
 
-@[inline] def getLCtx : MetaM LocalContext := do
-ctx ← read; pure ctx.lctx
+@[init] private def regTraceClasses : IO Unit := do
+registerTraceClass `Meta;
+registerTraceClass `Meta.debug
 
-@[inline] def getLocalInstances : MetaM LocalInstances := do
-ctx ← read; pure ctx.localInstances
+end Meta
 
-@[inline] def getConfig : MetaM Config := do
-ctx ← read; pure ctx.config
+export Meta (MetaM)
 
-@[inline] def getMCtx : MetaM MetavarContext := do
-s ← get; pure s.mctx
+class MonadMetaM (m : Type → Type) :=
+(liftMetaM {α} : MetaM α → m α)
 
-def setMCtx (mctx : MetavarContext) : MetaM Unit :=
-modify $ fun s => { s with mctx := mctx }
+export MonadMetaM (liftMetaM)
+
+instance monadMetaSelf : MonadMetaM MetaM :=
+{ liftMetaM := fun α x => x }
+
+-- TODO: uncomment after we switch to new frontend
+-- instance monadTrans (m n) [MonadMetaM m] [HasMonadLift m n] : MonadMetaM n :=
+-- { liftMetaM := fun α x => liftM (liftMetaM x : m _) }
+instance monadMetaReader (m ρ) [MonadMetaM m] : MonadMetaM (ReaderT ρ m) :=
+{ liftMetaM := fun α x _ => liftMetaM x }
+instance monadMetaStateRef (m ω σ) [MonadMetaM m] : MonadMetaM (StateRefT' ω σ m) :=
+{ liftMetaM := fun α x _ => liftMetaM x }
+instance monadMetaOption(m) [MonadMetaM m] [Monad m] : MonadMetaM (OptionT m) :=
+{ liftMetaM := fun α x => liftM (liftMetaM x : m _) }
+
+section Methods
+variables {m : Type → Type} [MonadMetaM m]
+
+def getLCtx : m LocalContext := liftMetaM do ctx ← read; pure ctx.lctx
+def getLocalInstances : m LocalInstances := liftMetaM do ctx ← read; pure ctx.localInstances
+def getConfig : m Meta.Config := liftMetaM do ctx ← read; pure ctx.config
+def getMCtx : m MetavarContext := liftMetaM do s ← get; pure s.mctx
+def setMCtx (mctx : MetavarContext) : m Unit := liftMetaM $ modify fun s => { s with mctx := mctx }
+@[inline] def modifyMCtx {m} [MonadMetaM m] (f : MetavarContext → MetavarContext) : m Unit := liftMetaM $ modify fun s => { s with mctx := f s.mctx }
 
 def mkWHNFRef : IO (IO.Ref (Expr → MetaM Expr)) :=
 IO.mkRef $ fun _ => throwError "whnf implementation was not set"
@@ -179,105 +200,86 @@ IO.mkRef $ fun _ => pure false
 
 @[init mkSynthPendingRef] def synthPendingRef : IO.Ref (MVarId → MetaM Bool) := arbitrary _
 
-def whnf (e : Expr) : MetaM Expr :=
-withIncRecDepth do
+def whnf (e : Expr) : m Expr :=
+liftMetaM $ withIncRecDepth do
   fn ← liftIO whnfRef.get;
   fn e
 
-def whnfForall (e : Expr) : MetaM Expr := do
+def whnfForall [Monad m] (e : Expr) : m Expr := do
 e' ← whnf e;
 if e'.isForall then pure e' else pure e
 
-def inferType (e : Expr) : MetaM Expr :=
-withIncRecDepth do
+def inferType (e : Expr) : m Expr :=
+liftMetaM $ withIncRecDepth do
   fn ← liftIO inferTypeRef.get;
   fn e
 
-def isExprDefEqAux (t s : Expr) : MetaM Bool :=
+protected def Meta.isExprDefEqAux (t s : Expr) : MetaM Bool :=
 withIncRecDepth do
   fn ← liftIO isExprDefEqAuxRef.get;
   fn t s
 
-def synthPending (mvarId : MVarId) : MetaM Bool :=
+protected def Meta.synthPending (mvarId : MVarId) : MetaM Bool :=
 withIncRecDepth do
   fn ← liftIO synthPendingRef.get;
   fn mvarId
 
 private def mkFreshExprMVarAtCore
     (mvarId : MVarId) (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (userName : Name) (kind : MetavarKind) : MetaM Expr := do
-modify $ fun s => { s with mctx := s.mctx.addExprMVarDecl mvarId userName lctx localInsts type kind };
+modifyMCtx fun mctx => mctx.addExprMVarDecl mvarId userName lctx localInsts type kind;
 pure $ mkMVar mvarId
 
 def mkFreshExprMVarAt
     (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural)
-    : MetaM Expr := do
+    : m Expr := liftMetaM do
 mvarId ← mkFreshId;
 mkFreshExprMVarAtCore mvarId lctx localInsts type userName kind
 
-def mkFreshExprMVar (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural) : MetaM Expr := do
+def mkFreshExprMVar (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural) : m Expr := liftMetaM do
 lctx ← getLCtx;
 localInsts ← getLocalInstances;
 mkFreshExprMVarAt lctx localInsts type userName kind
 
 /- Low-level version of `MkFreshExprMVar` which allows users to create/reserve a `mvarId` using `mkFreshId`, and then later create
    the metavar using this method. -/
-def mkFreshExprMVarWithId (mvarId : MVarId) (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural) : MetaM Expr := do
+def mkFreshExprMVarWithId (mvarId : MVarId) (type : Expr) (userName : Name := Name.anonymous) (kind : MetavarKind := MetavarKind.natural)
+    : m Expr := liftMetaM do
 lctx ← getLCtx;
 localInsts ← getLocalInstances;
 mkFreshExprMVarAtCore mvarId lctx localInsts type userName kind
 
-def mkFreshLevelMVar : MetaM Level := do
+def mkFreshLevelMVar : m Level := liftMetaM do
 mvarId ← mkFreshId;
-modify $ fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId };
+modifyMCtx fun mctx => mctx.addLevelMVarDecl mvarId;
 pure $ mkLevelMVar mvarId
 
-@[inline] def shouldReduceAll : MetaM Bool := do
-ctx ← read; pure $ ctx.config.transparency == TransparencyMode.all
-
-@[inline] def shouldReduceReducibleOnly : MetaM Bool := do
-ctx ← read; pure $ ctx.config.transparency == TransparencyMode.reducible
-
-@[inline] def getTransparency : MetaM TransparencyMode := do
+def shouldReduceAll : MetaM Bool := liftMetaM do
+ctx ← read; pure $ ctx.config.transparency == Meta.TransparencyMode.all
+def shouldReduceReducibleOnly : m Bool := liftMetaM do
+ctx ← read; pure $ ctx.config.transparency == Meta.TransparencyMode.reducible
+def getTransparency : m Meta.TransparencyMode := liftMetaM do
 ctx ← read; pure $ ctx.config.transparency
 
--- Remark: wanted to use `private`, but in C++ parser, `private` declarations do not shadow outer public ones.
+-- Remark: wanted to use `private`, but in the C++ parser, `private` declarations do not shadow outer public ones.
 -- TODO: fix this bug
-@[inline] def isReducible (constName : Name) : MetaM Bool := do
+protected def Meta.isReducible (constName : Name) : MetaM Bool := do
 env ← getEnv; pure $ isReducible env constName
 
-@[inline] def withConfig {α} (f : Config → Config) (x : MetaM α) : MetaM α :=
-adaptReader (fun (ctx : Context) => { ctx with config := f ctx.config }) x
-
-/-- While executing `x`, ensure the given transparency mode is used. -/
-@[inline] def withTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
-withConfig (fun config => { config with transparency := mode }) x
-
-@[inline] def withReducible {α} (x : MetaM α) : MetaM α :=
-withTransparency TransparencyMode.reducible x
-
-@[inline] def withAtLeastTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
-withConfig
-  (fun config =>
-    let oldMode := config.transparency;
-    let mode    := if oldMode.lt mode then mode else oldMode;
-    { config with transparency := mode })
-  x
-
-def getMVarDecl (mvarId : MVarId) : MetaM MetavarDecl := do
+def getMVarDecl (mvarId : MVarId) : m MetavarDecl := liftMetaM do
 mctx ← getMCtx;
 match mctx.findDecl? mvarId with
 | some d => pure d
 | none   => throwError ("unknown metavariable '" ++ mkMVar mvarId ++ "'")
 
-def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit :=
-modify $ fun s => { s with mctx := s.mctx.setMVarKind mvarId kind }
+def setMVarKind (mvarId : MVarId) (kind : MetavarKind) : m Unit :=
+modifyMCtx fun mctx => mctx.setMVarKind mvarId kind
 
-def isReadOnlyExprMVar (mvarId : MVarId) : MetaM Bool := do
+def isReadOnlyExprMVar (mvarId : MVarId) : m Bool := liftMetaM do
 mvarDecl ← getMVarDecl mvarId;
 mctx     ← getMCtx;
 pure $ mvarDecl.depth != mctx.depth
 
-def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : MetaM Bool := do
+def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : m Bool := liftMetaM do
 mvarDecl ← getMVarDecl mvarId;
 match mvarDecl.kind with
 | MetavarKind.syntheticOpaque => pure true
@@ -285,73 +287,46 @@ match mvarDecl.kind with
   mctx ← getMCtx;
   pure $ mvarDecl.depth != mctx.depth
 
-def isReadOnlyLevelMVar (mvarId : MVarId) : MetaM Bool := do
+def isReadOnlyLevelMVar (mvarId : MVarId) : m Bool := liftMetaM do
 mctx ← getMCtx;
 match mctx.findLevelDepth? mvarId with
 | some depth => pure $ depth != mctx.depth
 | _          => throwError ("unknown universe metavariable '" ++ mkLevelMVar mvarId ++ "'")
 
-def renameMVar (mvarId : MVarId) (newUserName : Name) : MetaM Unit :=
-modify $ fun s => { s with mctx := s.mctx.renameMVar mvarId newUserName }
+def renameMVar (mvarId : MVarId) (newUserName : Name) : m Unit :=
+modifyMCtx fun mctx => mctx.renameMVar mvarId newUserName
 
-@[inline] def isExprMVarAssigned (mvarId : MVarId) : MetaM Bool := do
+def isExprMVarAssigned (mvarId : MVarId) : m Bool := liftMetaM do
 mctx ← getMCtx;
 pure $ mctx.isExprAssigned mvarId
 
-@[inline] def getExprMVarAssignment? (mvarId : MVarId) : MetaM (Option Expr) := do
+def getExprMVarAssignment? (mvarId : MVarId) : m (Option Expr) := liftMetaM do
 mctx ← getMCtx; pure (mctx.getExprAssignment? mvarId)
 
-def assignExprMVar (mvarId : MVarId) (val : Expr) : MetaM Unit := do
-modify $ fun s => { s with mctx := s.mctx.assignExpr mvarId val }
+def assignExprMVar (mvarId : MVarId) (val : Expr) : m Unit := liftMetaM do
+modifyMCtx fun mctx => mctx.assignExpr mvarId val
 
-def isDelayedAssigned (mvarId : MVarId) : MetaM Bool := do
+def isDelayedAssigned (mvarId : MVarId) : m Bool := liftMetaM do
 mctx ← getMCtx;
 pure $ mctx.isDelayedAssigned mvarId
 
-def hasAssignableMVar (e : Expr) : MetaM Bool := do
+def hasAssignableMVar (e : Expr) : m Bool := liftMetaM do
 mctx ← getMCtx;
 pure $ mctx.hasAssignableMVar e
 
-def throwUnknownConstant {α} (constName : Name) : MetaM α :=
-throwError ("unknown constant '" ++ constName ++ "'")
-
-def getConst? (constName : Name) : MetaM (Option ConstantInfo) := do
-env ← getEnv;
-match env.find? constName with
-| some (info@(ConstantInfo.thmInfo _)) =>
-  condM shouldReduceAll (pure (some info)) (pure none)
-| some (info@(ConstantInfo.defnInfo _)) =>
-  condM shouldReduceReducibleOnly
-    (condM (isReducible constName) (pure (some info)) (pure none))
-    (pure (some info))
-| some info => pure (some info)
-| none      => throwUnknownConstant constName
-
-def getConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do
-env ← getEnv;
-match env.find? constName with
-| some (info@(ConstantInfo.thmInfo _)) =>
-  condM shouldReduceAll (pure (some info)) (pure none)
-| some (info@(ConstantInfo.defnInfo _)) =>
-  condM shouldReduceReducibleOnly
-    (condM (isReducible constName) (pure (some info)) (pure none))
-    (pure (some info))
-| some info => pure (some info)
-| none      => pure none
-
 def throwUnknownFVar {α} (fvarId : FVarId) : MetaM α :=
 throwError ("unknown free variable '" ++ mkFVar fvarId ++ "'")
 
-def getLocalDecl (fvarId : FVarId) : MetaM LocalDecl := do
+def getLocalDecl (fvarId : FVarId) : m LocalDecl := liftMetaM do
 lctx ← getLCtx;
 match lctx.find? fvarId with
 | some d => pure d
 | none   => throwUnknownFVar fvarId
 
-def getFVarLocalDecl (fvar : Expr) : MetaM LocalDecl :=
+def getFVarLocalDecl (fvar : Expr) : m LocalDecl := liftMetaM do
 getLocalDecl fvar.fvarId!
 
-def instantiateMVars (e : Expr) : MetaM Expr :=
+def instantiateMVars (e : Expr) : m Expr := liftMetaM do
 if e.hasMVar then
   modifyGet $ fun s =>
     let (e, mctx) := s.mctx.instantiateMVars e;
@@ -359,7 +334,7 @@ if e.hasMVar then
 else
   pure e
 
-def instantiateLocalDeclMVars (localDecl : LocalDecl) : MetaM LocalDecl :=
+def instantiateLocalDeclMVars (localDecl : LocalDecl) : m LocalDecl := liftMetaM do
 match localDecl with
   | LocalDecl.cdecl idx id n type bi  => do
     type ← instantiateMVars type;
@@ -383,18 +358,70 @@ match x lctx { mctx := mctx, ngen := ngen } with
   setNGen newS.ngen;
   throwError "failed to create binder due to failure when reverting variable dependencies"
 
-def mkForall (xs : Array Expr) (e : Expr) : MetaM Expr :=
+def mkForallFVars (xs : Array Expr) (e : Expr) : m Expr := liftMetaM do
 if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.mkForall xs e
 
-def mkLambda (xs : Array Expr) (e : Expr) : MetaM Expr :=
+def mkLambdaFVars (xs : Array Expr) (e : Expr) : m Expr := liftMetaM do
 if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.mkLambda xs e
 
-def mkForallUsedOnly (xs : Array Expr) (e : Expr) : MetaM (Expr × Nat) :=
+def mkLetFVars (xs : Array Expr) (e : Expr) : m Expr :=
+mkLambdaFVars xs e
+
+def mkForallUsedOnly (xs : Array Expr) (e : Expr) : m (Expr × Nat) := liftMetaM do
 if xs.isEmpty then pure (e, 0) else liftMkBindingM $ MetavarContext.mkForallUsedOnly xs e
 
-def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) : MetaM Expr :=
+def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) : m Expr := liftMetaM do
 if xs.isEmpty then pure e else liftMkBindingM $ MetavarContext.elimMVarDeps xs e preserveOrder
 
+end Methods
+
+namespace Meta
+
+@[inline] def withConfig {α} (f : Config → Config) (x : MetaM α) : MetaM α :=
+adaptReader (fun (ctx : Context) => { ctx with config := f ctx.config }) x
+
+/-- While executing `x`, ensure the given transparency mode is used. -/
+@[inline] def withTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
+withConfig (fun config => { config with transparency := mode }) x
+
+@[inline] def withReducible {α} (x : MetaM α) : MetaM α :=
+withTransparency TransparencyMode.reducible x
+
+@[inline] def withAtLeastTransparency {α} (mode : TransparencyMode) (x : MetaM α) : MetaM α :=
+withConfig
+  (fun config =>
+    let oldMode := config.transparency;
+    let mode    := if oldMode.lt mode then mode else oldMode;
+    { config with transparency := mode })
+  x
+
+def throwUnknownConstant {α} (constName : Name) : MetaM α :=
+throwError ("unknown constant '" ++ constName ++ "'")
+
+def getConst? (constName : Name) : MetaM (Option ConstantInfo) := do
+env ← getEnv;
+match env.find? constName with
+| some (info@(ConstantInfo.thmInfo _)) =>
+  condM shouldReduceAll (pure (some info)) (pure none)
+| some (info@(ConstantInfo.defnInfo _)) =>
+  condM shouldReduceReducibleOnly
+    (condM (Meta.isReducible constName) (pure (some info)) (pure none))
+    (pure (some info))
+| some info => pure (some info)
+| none      => throwUnknownConstant constName
+
+def getConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do
+env ← getEnv;
+match env.find? constName with
+| some (info@(ConstantInfo.thmInfo _)) =>
+  condM shouldReduceAll (pure (some info)) (pure none)
+| some (info@(ConstantInfo.defnInfo _)) =>
+  condM shouldReduceReducibleOnly
+    (condM (Meta.isReducible constName) (pure (some info)) (pure none))
+    (pure (some info))
+| some info => pure (some info)
+| none      => pure none
+
 /-- Save cache, execute `x`, restore cache -/
 @[inline] def savingCache {α} (x : MetaM α) : MetaM α := do
 s ← get;
@@ -700,37 +727,6 @@ private partial def lambdaMetaTelescopeAux (maxMVars? : Option Nat)
 def lambdaMetaTelescope (e : Expr) (maxMVars? : Option Nat := none) : MetaM (Array Expr × Array BinderInfo × Expr) :=
 lambdaMetaTelescopeAux maxMVars? #[] #[] 0 e
 
-@[inline] def liftStateMCtx {α} (x : StateM MetavarContext α) : MetaM α := do
-mctx ← getMCtx;
-let (a, mctx) := x.run mctx;
-modify fun s => { s with mctx := mctx };
-pure a
-
-def instantiateLevelMVars (lvl : Level) : MetaM Level :=
-liftStateMCtx $ MetavarContext.instantiateLevelMVars lvl
-
-def assignLevelMVar (mvarId : MVarId) (lvl : Level) : MetaM Unit :=
-modify $ fun s => { s with mctx := MetavarContext.assignLevel s.mctx mvarId lvl }
-
-def whnfD : Expr → MetaM Expr :=
-fun e => withTransparency TransparencyMode.default $ whnf e
-
-/-- Execute `x` using approximate unification: `foApprox`, `ctxApprox` and `quasiPatternApprox`.  -/
-@[inline] def approxDefEq {α} (x : MetaM α) : MetaM α :=
-adaptReader (fun (ctx : Context) => { ctx with config := { ctx.config with foApprox := true, ctxApprox := true, quasiPatternApprox := true} })
-  x
-
-/--
-  Similar to `approxDefEq`, but uses all available approximations.
-  We don't use `constApprox` by default at `approxDefEq` because it often produces undesirable solution for monadic code.
-  For example, suppose we have `pure (x > 0)` which has type `?m Prop`. We also have the goal `[HasPure ?m]`.
-  Now, assume the expected type is `IO Bool`. Then, the unification constraint `?m Prop =?= IO Bool` could be solved
-  as `?m := fun _ => IO Bool` using `constApprox`, but this spurious solution would generate a failure when we try to
-  solve `[HasPure (fun _ => IO Bool)]` -/
-@[inline] def fullApproxDefEq {α} (x : MetaM α) : MetaM α :=
-adaptReader (fun (ctx : Context) => { ctx with config := { ctx.config with foApprox := true, ctxApprox := true, quasiPatternApprox := true, constApprox := true } })
-  x
-
 @[inline] private def withNewFVar {α} (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM α := do
 c? ← isClass? fvarType;
 match c? with
@@ -803,28 +799,64 @@ mctx' ← getMCtx;
 modify $ fun s => { s with mctx := mctx };
 finally x (modify $ fun s => { s with mctx := mctx' })
 
+@[inline] def liftStateMCtx {α} (x : StateM MetavarContext α) : MetaM α := do
+mctx ← getMCtx;
+let (a, mctx) := x.run mctx;
+modify fun s => { s with mctx := mctx };
+pure a
+
+/-- Execute `x` using approximate unification: `foApprox`, `ctxApprox` and `quasiPatternApprox`.  -/
+@[inline] def approxDefEq {α} (x : MetaM α) : MetaM α :=
+adaptReader (fun (ctx : Context) => { ctx with config := { ctx.config with foApprox := true, ctxApprox := true, quasiPatternApprox := true} })
+  x
+
+/--
+  Similar to `approxDefEq`, but uses all available approximations.
+  We don't use `constApprox` by default at `approxDefEq` because it often produces undesirable solution for monadic code.
+  For example, suppose we have `pure (x > 0)` which has type `?m Prop`. We also have the goal `[HasPure ?m]`.
+  Now, assume the expected type is `IO Bool`. Then, the unification constraint `?m Prop =?= IO Bool` could be solved
+  as `?m := fun _ => IO Bool` using `constApprox`, but this spurious solution would generate a failure when we try to
+  solve `[HasPure (fun _ => IO Bool)]` -/
+@[inline] def fullApproxDefEq {α} (x : MetaM α) : MetaM α :=
+adaptReader (fun (ctx : Context) => { ctx with config := { ctx.config with foApprox := true, ctxApprox := true, quasiPatternApprox := true, constApprox := true } })
+  x
+
+end Meta
+
+section Methods
+variables {m : Type → Type} [MonadMetaM m]
+
+def instantiateLevelMVars (lvl : Level) : m Level :=
+liftMetaM $ Meta.liftStateMCtx $ MetavarContext.instantiateLevelMVars lvl
+
+def assignLevelMVar (mvarId : MVarId) (lvl : Level) : m Unit :=
+modifyMCtx fun mctx => mctx.assignLevel mvarId lvl
+
+def whnfD (e : Expr) : m Expr :=
+liftMetaM $ Meta.withTransparency Meta.TransparencyMode.default $ whnf e
+
 /--
   Create an auxiliary definition with the given name, type and value.
   The parameters `type` and `value` may contain free and meta variables.
   A "closure" is computed, and a term of the form `name.{u_1 ... u_n} t_1 ... t_m` is
   returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on,
   and `t_j`s are free and meta variables `type` and `value` depend on. -/
-def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM Expr := do
+def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := false) : m Expr := liftMetaM do
 env   ← getEnv;
 opts  ← getOptions;
 mctx  ← getMCtx;
 lctx  ← getLCtx;
-match Lean.mkAuxDefinition env opts mctx lctx name type value with
+match mkAuxDefinitionCore env opts mctx lctx name type value zeta with
 | Except.error ex          => throwKernelException ex
 | Except.ok (e, env, mctx) => do setEnv env; setMCtx mctx; pure e
 
 /-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/
-def mkAuxDefinitionFor (name : Name) (value : Expr) : MetaM Expr := do
+def mkAuxDefinitionFor (name : Name) (value : Expr) : m Expr := liftMetaM do
 type ← inferType value;
 let type := type.headBeta;
 mkAuxDefinition name type value
 
-def setInlineAttribute (declName : Name) (kind := Compiler.InlineAttributeKind.inline): MetaM Unit := do
+def setInlineAttribute (declName : Name) (kind := Compiler.InlineAttributeKind.inline): m Unit := liftMetaM do
 env ← getEnv;
 match Compiler.setInlineAttribute env declName kind with
 | Except.ok env    => setEnv env
@@ -842,15 +874,8 @@ private partial def instantiateForallAux (ps : Array Expr) : Nat → Expr → Me
     pure e
 
 /- Given `e` of the form `forall (a_1 : A_1) ... (a_n : A_n), B[a_1, ..., a_n]` and `p_1 : A_1, ... p_n : A_n`, return `B[p_1, ..., p_n]`. -/
-def instantiateForall (e : Expr) (ps : Array Expr) : MetaM Expr :=
-instantiateForallAux ps 0 e
-
-@[init] private def regTraceClasses : IO Unit := do
-registerTraceClass `Meta;
-registerTraceClass `Meta.debug
-
-end Meta
-
-export Meta (MetaM)
+def instantiateForall (e : Expr) (ps : Array Expr) : m Expr :=
+liftMetaM $ instantiateForallAux ps 0 e
 
+end Methods
 end Lean
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index 577bbddf5e..57014d1639 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -41,7 +41,7 @@ lambdaTelescope e $ fun xs b => do
       ensureType t;
       check t;
       vType ← inferType v;
-      unlessM (isExprDefEqAux t vType) $ throwLetTypeMismatchMessage x.fvarId!;
+      unlessM (Meta.isExprDefEqAux t vType) $ throwLetTypeMismatchMessage x.fvarId!;
       check v
   };
   check b
@@ -92,7 +92,7 @@ fType ← whnf fType;
 match fType with
 | Expr.forallE _ d _ _ => do
   aType ← inferType a;
-  unlessM (isExprDefEqAux d aType) $ throwAppTypeMismatch f a
+  unlessM (Meta.isExprDefEqAux d aType) $ throwAppTypeMismatch f a
 | _ => throwFunctionExpected (mkApp f a)
 
 private partial def checkAux : Expr → MetaM Unit
diff --git a/src/Lean/Meta/EqnCompiler/CaseArraySizes.lean b/src/Lean/Meta/EqnCompiler/CaseArraySizes.lean
index 1e24b08a3f..68a233cfd3 100644
--- a/src/Lean/Meta/EqnCompiler/CaseArraySizes.lean
+++ b/src/Lean/Meta/EqnCompiler/CaseArraySizes.lean
@@ -45,7 +45,7 @@ private partial def introArrayLitAux (mvarId : MVarId) (α : Expr) (a : Expr) (n
     aEqLitPrf ← mkAppM `Array.toArrayLitEq #[a, mkNatLit n, aSizeEqN];
     withLocalDecl `hEqALit aEqXsLit BinderInfo.default fun heq => do
       target    ← getMVarType mvarId;
-      newTarget ← mkForall (xs.push heq) target;
+      newTarget ← mkForallFVars (xs.push heq) target;
       pure (newTarget, args.push aEqLitPrf)
 
 private partial def introArrayLit (mvarId : MVarId) (a : Expr) (n : Nat) (xNamePrefix : Name) (aSizeEqN : Expr) : MetaM MVarId := do
diff --git a/src/Lean/Meta/EqnCompiler/Match.lean b/src/Lean/Meta/EqnCompiler/Match.lean
index 20dcabceb3..596376ba14 100644
--- a/src/Lean/Meta/EqnCompiler/Match.lean
+++ b/src/Lean/Meta/EqnCompiler/Match.lean
@@ -202,7 +202,7 @@ private partial def withAltsAux {α} (motive : Expr) : List AltLHS → List Alt
   minorType ← withExistingLocalDecls lhs.fvarDecls do {
     args ← lhs.patterns.toArray.mapM Pattern.toExpr;
     let minorType := mkAppN motive args;
-    mkForall xs minorType
+    mkForallFVars xs minorType
   };
   let minorType := if minorType.isForall then minorType else mkThunkType minorType;
   let idx       := alts.length;
@@ -387,7 +387,7 @@ else do
 partial def unify : Expr → Expr → M Bool
 | a, b => do
   trace! `Meta.EqnCompiler.matchUnify (a ++ " =?= " ++ b);
-  condM (liftM $ isDefEq a b) (pure true) do
+  condM (isDefEq a b) (pure true) do
   a' ← expandIfVar a;
   b' ← expandIfVar b;
   if a != a' || b != b' then unify a' b'
@@ -678,8 +678,8 @@ withAlts motive lhss fun alts minors => do
   let examples := majors.toList.map fun major => Example.var major.fvarId!;
   (_, s) ← (process { mvarId := mvar.mvarId!, vars := majors.toList, alts := alts, examples := examples }).run {};
   let args := #[motive] ++ majors ++ minors;
-  type ← mkForall args mvarType;
-  val  ← mkLambda args mvar;
+  type ← mkForallFVars args mvarType;
+  val  ← mkLambdaFVars args mvar;
   trace! `Meta.EqnCompiler.matchDebug ("eliminator value: " ++ val ++ "\ntype: " ++ type);
   elim ← mkAuxDefinition elimName type val;
   setInlineAttribute elimName;
@@ -715,7 +715,7 @@ else do
 def mkElimTester (elimName : Name) (majors : List Expr) (lhss : List AltLHS) (inProp : Bool := false) : MetaM ElimResult := do
 sortv ← mkElimSort majors lhss inProp;
 generalizeTelescope majors.toArray `_d fun majors => do
-  motiveType ← mkForall majors sortv;
+  motiveType ← mkForallFVars majors sortv;
   mkElim elimName motiveType lhss
 
 @[init] private def regTraceClasses : IO Unit := do
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 27bcf904c7..599ca91b34 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -29,15 +29,15 @@ if a.isLambda && !b.isLambda then do
   bType ← whnfD bType;
   match bType with
   | Expr.forallE n d _ c =>
-    let b' := Lean.mkLambda n c.binderInfo d (mkApp b (mkBVar 0));
-    commitWhen $ isExprDefEqAux a b'
+    let b' := mkLambda n c.binderInfo d (mkApp b (mkBVar 0));
+    commitWhen $ Meta.isExprDefEqAux a b'
   | _ => pure false
 else
   pure false
 
 /-- Support for `Lean.reduceBool` and `Lean.reduceNat` -/
 def isDefEqNative (s t : Expr) : MetaM LBool := do
-let isDefEq (s t) : MetaM LBool := toLBoolM $ isExprDefEqAux s t;
+let isDefEq (s t) : MetaM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
 s? ← reduceNative? s;
 t? ← reduceNative? t;
 match s?, t? with
@@ -48,7 +48,7 @@ match s?, t? with
 
 /-- Support for reducing Nat basic operations. -/
 def isDefEqNat (s t : Expr) : MetaM LBool := do
-let isDefEq (s t) : MetaM LBool := toLBoolM $ isExprDefEqAux s t;
+let isDefEq (s t) : MetaM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
 if s.hasFVar || s.hasMVar || t.hasFVar || t.hasMVar then
   pure LBool.undef
 else do
@@ -62,7 +62,7 @@ else do
 
 /-- Support for constraints of the form `("..." =?= String.mk cs)` -/
 def isDefEqStringLit (s t : Expr) : MetaM LBool := do
-let isDefEq (s t) : MetaM LBool := toLBoolM $ isExprDefEqAux s t;
+let isDefEq (s t) : MetaM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
 if s.isStringLit && t.isAppOf `String.mk then
   isDefEq (WHNF.toCtorIfLit s) t
 else if s.isAppOf `String.mk && t.isStringLit then
@@ -122,12 +122,12 @@ private partial def isDefEqArgsFirstPass
     let a₂ := args₂.get! i;
     if info.implicit || info.instImplicit then
       condM (isEtaUnassignedMVar a₁ <||> isEtaUnassignedMVar a₂)
-        (condM (isExprDefEqAux a₁ a₂)
+        (condM (Meta.isExprDefEqAux a₁ a₂)
           (isDefEqArgsFirstPass (i+1) postponed)
           (pure none))
         (isDefEqArgsFirstPass (i+1) (postponed.push i))
     else
-      condM (isExprDefEqAux a₁ a₂)
+      condM (Meta.isExprDefEqAux a₁ a₂)
         (isDefEqArgsFirstPass (i+1) postponed)
         (pure none)
   else
@@ -138,7 +138,7 @@ private partial def isDefEqArgsAux (args₁ args₂ : Array Expr) (h : args₁.s
   if h₁ : i < args₁.size then
     let a₁ := args₁.get ⟨i, h₁⟩;
     let a₂ := args₂.get ⟨i, h ▸ h₁⟩;
-    condM (isExprDefEqAux a₁ a₂)
+    condM (Meta.isExprDefEqAux a₁ a₂)
       (isDefEqArgsAux (i+1))
       (pure false)
   else
@@ -147,7 +147,7 @@ private partial def isDefEqArgsAux (args₁ args₂ : Array Expr) (h : args₁.s
 @[specialize] private def trySynthPending (e : Expr) : MetaM Bool := do
 mvarId? ← getStuckMVar? e;
 match mvarId? with
-| some mvarId => synthPending mvarId
+| some mvarId => Meta.synthPending mvarId
 | none        => pure false
 
 private def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : MetaM Bool :=
@@ -168,7 +168,7 @@ if h : args₁.size = args₂.size then do
       _ ← trySynthPending a₂;
       pure ()
     };
-    withAtLeastTransparency TransparencyMode.default $ isExprDefEqAux a₁ a₂)
+    withAtLeastTransparency TransparencyMode.default $ Meta.isExprDefEqAux a₁ a₂)
 else
   pure false
 
@@ -190,7 +190,7 @@ else
     fvarDecl ← getFVarLocalDecl fvar;
     let fvarType := fvarDecl.type;
     let d₂       := ds₂.get! i;
-    condM (isExprDefEqAux fvarType d₂)
+    condM (Meta.isExprDefEqAux fvarType d₂)
       (do c? ← isClass? fvarType;
           match c? with
           | some className => withNewLocalInstance className fvar $ isDefEqBindingDomain (i+1) k
@@ -219,7 +219,7 @@ private partial def isDefEqBindingAux : LocalContext → Array Expr → Expr →
   | _,                      _                      =>
     adaptReader (fun (ctx : Context) => { ctx with lctx := lctx }) $
       isDefEqBindingDomain fvars ds₂ 0 $
-        isExprDefEqAux (e₁.instantiateRev fvars) (e₂.instantiateRev fvars)
+        Meta.isExprDefEqAux (e₁.instantiateRev fvars) (e₂.instantiateRev fvars)
 
 @[inline] private def isDefEqBinding (a b : Expr) : MetaM Bool := do
 lctx ← getLCtx;
@@ -230,7 +230,7 @@ traceCtx `Meta.isDefEq.assign.checkTypes $ do
   -- must check whether types are definitionally equal or not, before assigning and returning true
   mvarType ← inferType mvar;
   vType    ← inferType v;
-  condM (withTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
+  condM (withTransparency TransparencyMode.default $ Meta.isExprDefEqAux mvarType vType)
     (do trace! `Meta.isDefEq.assign.final (mvar ++ " := " ++ v);
         assignExprMVar mvar.mvarId! v; pure true)
     (do trace `Meta.isDefEq.assign.typeMismatch $ fun _ => mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType;
@@ -407,11 +407,8 @@ else do
       traceM `Meta.isDefEq.assign.outOfScopeFVar $ addAssignmentInfo fvar;
       throwOutOfScopeFVar
 
-@[inline] def getMCtx : CheckAssignmentM MetavarContext := do
-liftM Meta.getMCtx
-
 def mkAuxMVar (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) : CheckAssignmentM Expr := do
-liftM $ mkFreshExprMVarAt lctx localInsts type
+mkFreshExprMVarAt lctx localInsts type
 
 @[specialize] def checkMVar (check : Expr → CheckAssignmentM Expr) (mvar : Expr) : CheckAssignmentM Expr := do
 let mvarId := mvar.mvarId!;
@@ -458,7 +455,7 @@ mvarType ← inferType mvar;
 forallBoundedTelescope mvarType numArgs $ fun xs _ =>
   if xs.size != numArgs then pure false
   else do
-    v ← mkLambda xs newMVar;
+    v ← mkLambdaFVars xs newMVar;
     checkTypesAndAssign mvar v
 
 partial def check : Expr → CheckAssignmentM Expr
@@ -483,8 +480,8 @@ partial def check : Expr → CheckAssignmentM Expr
         args ← args.mapM (visit check);
         pure $ mkAppN f args)
       (fun ex =>
-        condM (liftM $ isDelayedAssigned f.mvarId!) (throw ex) do
-          eType ← liftM $ inferType e;
+        condM (isDelayedAssigned f.mvarId!) (throw ex) do
+          eType ← inferType e;
           mvarType ← check eType;
           /- Create an auxiliary metavariable with a smaller context and "checked" type, assign `?f := fun _ => ?newMVar`
                Note that `mvarType` may be different from `eType`. -/
@@ -580,7 +577,7 @@ else do
 
 private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : MetaM Bool :=
 match v with
-| Expr.app f a _ => isExprDefEqAux args.back a <&&> isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f
+| Expr.app f a _ => Meta.isExprDefEqAux args.back a <&&> Meta.isExprDefEqAux (mkAppRange mvar 0 (args.size - 1) args) f
 | _              => pure false
 
 /-
@@ -640,7 +637,7 @@ if cfg.constApprox then do
     forallBoundedTelescope mvarDecl.type numArgs $ fun xs _ =>
       if xs.size != numArgs then pure false
       else do
-        v ← mkLambda xs v;
+        v ← mkLambdaFVars xs v;
         checkTypesAndAssign mvar v
 else
   pure false
@@ -676,9 +673,9 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
       | none   => useFOApprox args
       | some v => do
         trace `Meta.isDefEq.assign.beforeMkLambda $ fun _ => mvar ++ " " ++ args ++ " := " ++ v;
-        v ← mkLambda args v;
+        v ← mkLambdaFVars args v;
         if args.any (fun arg => mvarDecl.lctx.containsFVar arg) then
-          /- We need to type check `v` because abstraction using `mkLambda` may have produced
+          /- We need to type check `v` because abstraction using `mkLambdaFVars` may have produced
              a type incorrect term. See discussion at A2 -/
           condM (isTypeCorrect v)
             (checkTypesAndAssign mvar v)
@@ -708,17 +705,17 @@ toLBoolM $ isListLevelDefEqAux us vs
 /-- Auxiliary method for isDefEqDelta -/
 private def isDefEqLeft (fn : Name) (t s : Expr) : MetaM LBool := do
 trace! `Meta.isDefEq.delta.unfoldLeft fn;
-toLBoolM $ isExprDefEqAux t s
+toLBoolM $ Meta.isExprDefEqAux t s
 
 /-- Auxiliary method for isDefEqDelta -/
 private def isDefEqRight (fn : Name) (t s : Expr) : MetaM LBool := do
 trace! `Meta.isDefEq.delta.unfoldRight fn;
-toLBoolM $ isExprDefEqAux t s
+toLBoolM $ Meta.isExprDefEqAux t s
 
 /-- Auxiliary method for isDefEqDelta -/
 private def isDefEqLeftRight (fn : Name) (t s : Expr) : MetaM LBool := do
 trace! `Meta.isDefEq.delta.unfoldLeftRight fn;
-toLBoolM $ isExprDefEqAux t s
+toLBoolM $ Meta.isExprDefEqAux t s
 
 /-- Try to solve `f a₁ ... aₙ =?= f b₁ ... bₙ` by solving `a₁ =?= b₁, ..., aₙ =?= bₙ`.
 
@@ -810,8 +807,8 @@ else
 private def unfoldReducibeDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : MetaM LBool :=
 condM shouldReduceReducibleOnly
   (unfoldDefEq tInfo sInfo t s)
-  (do tReducible ← isReducible tInfo.name;
-      sReducible ← isReducible sInfo.name;
+  (do tReducible ← Meta.isReducible tInfo.name;
+      sReducible ← Meta.isReducible sInfo.name;
       if tReducible && !sReducible then
         unfold t (unfoldDefEq tInfo sInfo t s) $ fun t => isDefEqLeft tInfo.name t s
       else if !tReducible && sReducible then
@@ -914,11 +911,11 @@ match status with
 | LBool.true  => do
   tType ← inferType t;
   sType ← inferType s;
-  toLBoolM $ isExprDefEqAux tType sType
+  toLBoolM $ Meta.isExprDefEqAux tType sType
 | LBool.undef => do
   tType ← inferType t;
   condM (isProp tType)
-    (do sType ← inferType s; toLBoolM $ isExprDefEqAux tType sType)
+    (do sType ← inferType s; toLBoolM $ Meta.isExprDefEqAux tType sType)
     (pure LBool.undef)
 
 private partial def isDefEqQuick : Expr → Expr → MetaM LBool
@@ -995,14 +992,14 @@ else
 mvarId? ← getStuckMVar? e;
 match mvarId? with
 | some mvarId =>
-  condM (synthPending mvarId)
+  condM (Meta.synthPending mvarId)
     (do e ← instantiateMVars e; successK e)
     failK
 | none   => failK
 
 private def isDefEqOnFailure (t s : Expr) : MetaM Bool :=
-unstuckMVar t (fun t => isExprDefEqAux t s) $
-unstuckMVar s (fun s => isExprDefEqAux t s) $
+unstuckMVar t (fun t => Meta.isExprDefEqAux t s) $
+unstuckMVar s (fun s => Meta.isExprDefEqAux t s) $
 pure false
 
 /- Remove unnecessary let-decls -/
@@ -1019,15 +1016,15 @@ partial def isExprDefEqAuxImpl : Expr → Expr → MetaM Bool
   whenUndefDo (isDefEqProofIrrel t s) $
   isDefEqWHNF t s $ fun t s => do
   condM (isDefEqEta t s <||> isDefEqEta s t) (pure true) $
-  whenUndefDo (isDefEqNative t s) $ do
-  whenUndefDo (isDefEqNat t s) $ do
-  whenUndefDo (isDefEqOffset t s) $ do
+  whenUndefDo (isDefEqNative t s) do
+  whenUndefDo (isDefEqNat t s) do
+  whenUndefDo (isDefEqOffset t s) do
   whenUndefDo (isDefEqDelta t s) $
   match t, s with
   | Expr.const c us _, Expr.const d vs _ => if c == d then isListLevelDefEqAux us vs else pure false
   | Expr.app _ _ _,    Expr.app _ _ _    =>
     let tFn := t.getAppFn;
-    condM (commitWhen (isExprDefEqAux tFn s.getAppFn <&&> isDefEqArgs tFn t.getAppArgs s.getAppArgs))
+    condM (commitWhen (Meta.isExprDefEqAux tFn s.getAppFn <&&> isDefEqArgs tFn t.getAppArgs s.getAppArgs))
       (pure true)
       (isDefEqOnFailure t s)
   | _, _ =>
diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index 75a906d039..0cca1dccec 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -103,7 +103,7 @@ forallTelescope e $ fun xs e => do
 private def inferLambdaType (e : Expr) : MetaM Expr :=
 lambdaTelescope e $ fun xs e => do
   type ← inferType e;
-  mkForall xs type
+  mkForallFVars xs type
 
 @[inline] private def withLocalDecl {α} (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α :=
 savingCache $ do
@@ -217,7 +217,7 @@ partial def isPropQuick : Expr → MetaM LBool
      to decide whether is a proposition or not. We return `false` in this
      case. We considered using `LBool` and retuning `LBool.undef`, but
      we have no applications for it. -/
-def isProp (e : Expr) : MetaM Bool := do
+protected def isProp (e : Expr) : MetaM Bool := do
 r ← isPropQuick e;
 match r with
 | LBool.true  => pure true
@@ -273,14 +273,14 @@ partial def isProofQuick : Expr → MetaM LBool
 | Expr.app f _ _        => isProofQuickApp isProofQuick f 1
 | Expr.localE _ _ _ _   => unreachable!
 
-def isProof (e : Expr) : MetaM Bool := do
+protected def isProof (e : Expr) : MetaM Bool := do
 r ← isProofQuick e;
 match r with
 | LBool.true  => pure true
 | LBool.false => pure false
 | LBool.undef => do
   type ← inferType e;
-  isProp type
+  Meta.isProp type
 
 /--
   `isArrowType type n` is an "approximate" predicate which returns `LBool.true`
@@ -326,7 +326,7 @@ partial def isTypeQuick : Expr → MetaM LBool
 | Expr.app f _ _        => isTypeQuickApp f 1
 | Expr.localE _ _ _ _   => unreachable!
 
-def isType (e : Expr) : MetaM Bool := do
+protected def isType {m} [MonadMetaM m] (e : Expr) : m Bool := liftMetaM do
 r ← isTypeQuick e;
 match r with
 | LBool.true  => pure true
@@ -338,7 +338,7 @@ match r with
   | Expr.sort _ _ => pure true
   | _             => pure false
 
-partial def isTypeFormerType : Expr → MetaM Bool
+protected partial def isTypeFormerType : Expr → MetaM Bool
 | type => do
   type ← whnfD type;
   match type with
@@ -348,12 +348,25 @@ partial def isTypeFormerType : Expr → MetaM Bool
     isTypeFormerType (b.instantiate1 fvar)
   | _ => pure false
 
+end Meta
+
+def isProp {m} [MonadMetaM m] (e : Expr) : m Bool :=
+liftMetaM $ Meta.isProp e
+
+def isProof {m} [MonadMetaM m] (e : Expr) : m Bool :=
+liftMetaM $ Meta.isProof e
+
+def isType {m} [MonadMetaM m] (e : Expr) : m Bool :=
+liftMetaM $ Meta.isType e
+
+def isTypeFormerType {m} [MonadMetaM m] (e : Expr) : m Bool :=
+liftMetaM $ Meta.isTypeFormerType e
+
 /--
   Return true iff `e : Sort _` or `e : (forall As, Sort _)`.
   Remark: it subsumes `isType` -/
-def isTypeFormer (e : Expr) : MetaM Bool := do
+def isTypeFormer {m} [MonadMetaM m] (e : Expr) : m Bool := liftMetaM do
 type ← inferType e;
 isTypeFormerType type
 
-end Meta
 end Lean
diff --git a/src/Lean/Meta/KAbstract.lean b/src/Lean/Meta/KAbstract.lean
index d09a71a53d..fe88e04c86 100644
--- a/src/Lean/Meta/KAbstract.lean
+++ b/src/Lean/Meta/KAbstract.lean
@@ -10,9 +10,9 @@ import Lean.Meta.ExprDefEq
 namespace Lean
 namespace Meta
 
-private partial def kabstractAux (occs : Occurrences) (p : Expr) (pHeadIdx : HeadIndex) (pNumArgs : Nat) : Expr → Nat → StateT Nat MetaM Expr
+private partial def kabstractAux (occs : Occurrences) (p : Expr) (pHeadIdx : HeadIndex) (pNumArgs : Nat) : Expr → Nat → StateRefT Nat MetaM Expr
 | e, offset =>
-  let visitChildren : Unit → StateT Nat MetaM Expr := fun _ =>
+  let visitChildren : Unit → StateRefT Nat MetaM Expr := fun _ =>
     match e with
     | Expr.app f a _       => do f ← kabstractAux f offset; a ← kabstractAux a offset; pure $ e.updateApp! f a
     | Expr.mdata _ b _     => do b ← kabstractAux b offset; pure $ e.updateMData! b
@@ -23,7 +23,7 @@ private partial def kabstractAux (occs : Occurrences) (p : Expr) (pHeadIdx : Hea
     | e                    => pure e;
   if e.hasLooseBVars then visitChildren ()
   else if e.toHeadIndex == pHeadIdx && e.headNumArgs == pNumArgs then
-    condM (liftM $ isDefEq e p)
+    condM (isDefEq e p)
       (do i ← get;
           set (i+1);
           if occs.contains i then
@@ -34,7 +34,7 @@ private partial def kabstractAux (occs : Occurrences) (p : Expr) (pHeadIdx : Hea
   else
     visitChildren ()
 
-def kabstract (e : Expr) (p : Expr) (occs : Occurrences := Occurrences.all) : MetaM Expr :=
+def kabstract {m} [MonadMetaM m] (e : Expr) (p : Expr) (occs : Occurrences := Occurrences.all) : m Expr := liftMetaM do
 (kabstractAux occs p p.toHeadIndex p.headNumArgs e 0).run' 1
 
 end Meta
diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean
index ae03feb05e..96b6635f9d 100644
--- a/src/Lean/Meta/LevelDefEq.lean
+++ b/src/Lean/Meta/LevelDefEq.lean
@@ -224,26 +224,34 @@ match r? with
 | some _ => pure true
 | none   => pure false
 
-/- Public interface -/
-
-def isLevelDefEq (u v : Level) : MetaM Bool :=
-traceCtx `Meta.isLevelDefEq $ do
-  b ← commitWhen $ isLevelDefEqAux u v;
-  trace! `Meta.isLevelDefEq (u ++ " =?= " ++ v ++ " ... " ++ if b then "success" else "failure");
-  pure b
-
-def isExprDefEq (t s : Expr) : MetaM Bool :=
-traceCtx `Meta.isDefEq $ do
-  b ← commitWhen $ isExprDefEqAux t s;
-  trace! `Meta.isDefEq (t ++ " =?= " ++ s ++ " ... " ++ if b then "success" else "failure");
-  pure b
-
-abbrev isDefEq := @isExprDefEq
-
 @[init] private def regTraceClasses : IO Unit := do
 registerTraceClass `Meta.isLevelDefEq;
 registerTraceClass `Meta.isLevelDefEq.step;
 registerTraceClass `Meta.isLevelDefEq.postponed
 
 end Meta
+
+/- Public interface -/
+section Methods
+variables {m : Type → Type} [MonadMetaM m]
+
+def isLevelDefEq (u v : Level) : m Bool := liftMetaM do
+traceCtx `Meta.isLevelDefEq $ do
+  b ← Meta.commitWhen $ Meta.isLevelDefEqAux u v;
+  trace! `Meta.isLevelDefEq (u ++ " =?= " ++ v ++ " ... " ++ if b then "success" else "failure");
+  pure b
+
+def isExprDefEq (t s : Expr) : m Bool := liftMetaM do
+traceCtx `Meta.isDefEq $ do
+  b ← Meta.commitWhen $ Meta.isExprDefEqAux t s;
+  trace! `Meta.isDefEq (t ++ " =?= " ++ s ++ " ... " ++ if b then "success" else "failure");
+  pure b
+
+abbrev isDefEq (t s : Expr) : m Bool :=
+isExprDefEq t s
+
+def isDefEqNoConstantApprox (t s : Expr) : m Bool := liftMetaM do
+Meta.approxDefEq $ isDefEq t s
+
+end Methods
 end Lean
diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean
index 33b9eb5c6f..3c1666108f 100644
--- a/src/Lean/Meta/Offset.lean
+++ b/src/Lean/Meta/Offset.lean
@@ -99,7 +99,7 @@ else if isNatZero e then mkNatLit offset
 else mkAppB (mkConst `Nat.add) e (mkNatLit offset)
 
 def isDefEqOffset (s t : Expr) : MetaM LBool :=
-let isDefEq (s t) : MetaM LBool := toLBoolM $ isExprDefEqAux s t;
+let isDefEq (s t) : MetaM LBool := toLBoolM $ Meta.isExprDefEqAux s t;
 match isOffset s with
 | some (s, k₁) => match isOffset t with
   | some (t, k₂) => -- s+k₁ =?= t+k₂
diff --git a/src/Lean/Meta/Reduce.lean b/src/Lean/Meta/Reduce.lean
index 7c3c947f68..5f60df5268 100644
--- a/src/Lean/Meta/Reduce.lean
+++ b/src/Lean/Meta/Reduce.lean
@@ -32,8 +32,8 @@ partial def reduceAux (explicitOnly : Bool) (skipTypes : Bool) (skipProofs : Boo
             args.modifyM i reduceAux)
         args;
       pure $ mkAppN f args
-    | Expr.lam _ _ _ _     => lambdaTelescope e $ fun xs b => do b ← reduceAux b; mkLambda xs b
-    | Expr.forallE _ _ _ _ => forallTelescope e $ fun xs b => do b ← reduceAux b; mkForall xs b
+    | Expr.lam _ _ _ _     => lambdaTelescope e $ fun xs b => do b ← reduceAux b; mkLambdaFVars xs b
+    | Expr.forallE _ _ _ _ => forallTelescope e $ fun xs b => do b ← reduceAux b; mkForallFVars xs b
     | _ => pure e
 
 def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : MetaM Expr :=
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 8b25392c80..e46960bc79 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -229,8 +229,8 @@ match entry? with
   We must instantiate assigned metavariables before we invoke `mkTableKey`. -/
 def mkTableKeyFor (mctx : MetavarContext) (mvar : Expr) : SynthM Expr :=
 withMCtx mctx $ do
-  mvarType ← liftM $ inferType mvar;
-  mvarType ← liftM $ instantiateMVars mvarType;
+  mvarType ← inferType mvar;
+  mvarType ← instantiateMVars mvarType;
   pure $ mkTableKey mctx mvarType
 
 /- See `getSubgoals` and `getSubgoalsAux`
@@ -248,7 +248,7 @@ private partial def getSubgoalsAux (lctx : LocalContext) (localInsts : LocalInst
     : Array Expr → Nat → List Expr → Expr → Expr → MetaM SubgoalsResult
 | args, j, subgoals, instVal, Expr.forallE n d b c => do
   let d        := d.instantiateRevRange j args.size args;
-  mvarType ← mkForall xs d;
+  mvarType ← mkForallFVars xs d;
   mvar     ← mkFreshExprMVarAt lctx localInsts mvarType;
   let arg      := mkAppN mvar xs;
   let instVal  := mkApp instVal arg;
@@ -298,7 +298,7 @@ forallTelescopeReducing mvarType $ fun xs mvarTypeBody => do
   ⟨subgoals, instVal, instTypeBody⟩ ← getSubgoals lctx localInsts xs inst;
   trace! `Meta.synthInstance.tryResolve (mvarTypeBody ++ " =?= " ++ instTypeBody);
   condM (isDefEq mvarTypeBody instTypeBody)
-    (do instVal ← mkLambda xs instVal;
+    (do instVal ← mkLambdaFVars xs instVal;
         condM (isDefEq mvar instVal)
           (do trace! `Meta.synthInstance.tryResolve "success";
               mctx ← getMCtx;
@@ -482,7 +482,7 @@ the original type `C a_1 ... a_n` witht the normalized one.
 private def preprocess (type : Expr) : MetaM Expr :=
 forallTelescopeReducing type $ fun xs type => do
   type ← whnf type;
-  mkForall xs type
+  mkForallFVars xs type
 
 private def preprocessLevels (us : List Level) : MetaM (List Level) := do
 us ← us.foldlM
@@ -523,7 +523,7 @@ forallTelescope type $ fun xs typeBody =>
       let c := mkConst constName us;
       cType ← inferType c;
       args ← preprocessArgs cType 0 args;
-      mkForall xs (mkAppN c args)
+      mkForallFVars xs (mkAppN c args)
   | _ => pure type
 
 @[init] def maxStepsOption : IO Unit :=
diff --git a/src/Lean/Meta/Tactic/Cases.lean b/src/Lean/Meta/Tactic/Cases.lean
index a20154485e..0445c55c46 100644
--- a/src/Lean/Meta/Tactic/Cases.lean
+++ b/src/Lean/Meta/Tactic/Cases.lean
@@ -99,9 +99,9 @@ withMVarContext mvarId $ do
       /- auxType `forall (j' : J) (h' : I A j'), j == j' -> h == h' -> target -/
       target  ← getMVarType mvarId;
       tag     ← getMVarTag mvarId;
-      auxType ← mkForall newEqs target;
-      auxType ← mkForall #[h'] auxType;
-      auxType ← mkForall newIndices auxType;
+      auxType ← mkForallFVars newEqs target;
+      auxType ← mkForallFVars #[h'] auxType;
+      auxType ← mkForallFVars newIndices auxType;
       newMVar ← mkFreshExprMVarAt lctx localInsts auxType tag MetavarKind.syntheticOpaque;
       /- assign mvarId := newMVar indices h refls -/
       assignExprMVar mvarId (mkAppN (mkApp (mkAppN newMVar indices) fvarDecl.toExpr) newRefls);
diff --git a/src/Lean/Meta/Tactic/Induction.lean b/src/Lean/Meta/Tactic/Induction.lean
index 5965099f0b..7763f515b7 100644
--- a/src/Lean/Meta/Tactic/Induction.lean
+++ b/src/Lean/Meta/Tactic/Induction.lean
@@ -204,8 +204,8 @@ withMVarContext mvarId $ do
           rec ← addRecParams mvarId majorTypeArgs recInfo.paramsPos rec;
           -- Compute motive
           let motive := target;
-          motive ← if recInfo.depElim then mkLambda #[major] motive else pure motive;
-          motive ← mkLambda indices motive;
+          motive ← if recInfo.depElim then mkLambdaFVars #[major] motive else pure motive;
+          motive ← mkLambdaFVars indices motive;
           let rec := mkApp rec motive;
           finalize mvarId givenNames recInfo reverted major indices baseSubst rec
         | _ =>
diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean
index 3f003be6d1..a67f33d690 100644
--- a/src/Lean/Meta/Tactic/Intro.lean
+++ b/src/Lean/Meta/Tactic/Intro.lean
@@ -19,7 +19,7 @@ def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ
       let type := type.headBeta;
       newMVar ← mkFreshExprSyntheticOpaqueMVar type tag;
       lctx    ← getLCtx;
-      newVal  ← mkLambda fvars newMVar;
+      newVal  ← mkLambdaFVars fvars newMVar;
       assignExprMVar mvarId newVal;
       pure $ (fvars, newMVar.mvarId!)
 | (i+1), lctx, fvars, j, s, Expr.letE n type val body _ => do
diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean
index a3d38efbc5..f8d6437035 100644
--- a/src/Lean/Meta/Tactic/Subst.lean
+++ b/src/Lean/Meta/Tactic/Subst.lean
@@ -79,7 +79,7 @@ withMVarContext mvarId $ do
             reflB ← mkEqRefl b;
             let newType := newType.replaceFVar h reflB;
             if symm then do
-              motive ← mkLambda #[a, h] type;
+              motive ← mkLambdaFVars #[a, h] type;
               continue motive newType
             else do
               /- `type` depends on (h : a = b). So, we use the following trick to avoid a type incorrect motive.
@@ -92,11 +92,11 @@ withMVarContext mvarId $ do
                 hAuxSymm ← mkEqSymm hAux;
                 /- replace h in type with hAuxSymm -/
                 let newType := type.replaceFVar h hAuxSymm;
-                mkLambda #[a, hAux] newType
+                mkLambdaFVars #[a, hAux] newType
               };
               continue motive newType
           else do
-            motive ← mkLambda #[a] type;
+            motive ← mkLambdaFVars #[a] type;
             let newType := type.replaceFVar a b;
             continue motive newType
     | _ =>
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index 90184079e9..4e05a7283c 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -11,14 +11,14 @@ import Lean.Meta.LevelDefEq
 namespace Lean
 namespace Meta
 
-def isAuxDef? (constName : Name) : MetaM Bool := do
+protected def isAuxDef? (constName : Name) : MetaM Bool := do
 env ← getEnv; pure (isAuxRecursor env constName || isNoConfusion env constName)
 
-def unfoldDefinition? (e : Expr) : MetaM (Option Expr)  :=
-Lean.WHNF.unfoldDefinitionAux getConstNoEx? isAuxDef? whnf inferType isExprDefEq synthPending getLocalDecl getExprMVarAssignment? e
+protected def unfoldDefinition? (e : Expr) : MetaM (Option Expr)  :=
+Lean.WHNF.unfoldDefinitionAux getConstNoEx? Meta.isAuxDef? whnf inferType isExprDefEq Meta.synthPending getLocalDecl getExprMVarAssignment? e
 
-def whnfCore (e : Expr) : MetaM Expr :=
-Lean.WHNF.whnfCore getConstNoEx? isAuxDef? whnf inferType isExprDefEqAux getLocalDecl getExprMVarAssignment? e
+protected def whnfCore (e : Expr) : MetaM Expr :=
+Lean.WHNF.whnfCore getConstNoEx? Meta.isAuxDef? whnf inferType Meta.isExprDefEqAux getLocalDecl getExprMVarAssignment? e
 
 unsafe def reduceNativeConst (α : Type) (typeName : Name) (constName : Name) : MetaM α := do
 env ← getEnv;
@@ -119,7 +119,7 @@ partial def whnfImpl : Expr → MetaM Expr
   match e? with
   | some e' => pure e'
   | none    => do
-    e' ← whnfCore e;
+    e' ← Meta.whnfCore e;
     v? ← reduceNat? e';
     match v? with
     | some v => cache useCache e v
@@ -128,7 +128,7 @@ partial def whnfImpl : Expr → MetaM Expr
       match v? with
       | some v => cache useCache e v
       | none => do
-        e? ← unfoldDefinition? e';
+        e? ← Meta.unfoldDefinition? e';
         match e? with
         | some e => whnfImpl e
         | none   => cache useCache e e'
@@ -153,27 +153,41 @@ match e.getAppFn with
   | _ => pure none
 | _ => pure none
 
-@[specialize] private partial def whnfHeadPredAux (pred : Expr → MetaM Bool) : Expr → MetaM Expr
+@[specialize] partial def whnfHeadPredAux (pred : Expr → MetaM Bool) : Expr → MetaM Expr
 | e => Lean.WHNF.whnfEasyCases getLocalDecl getExprMVarAssignment? e $ fun e => do
-  e ← whnfCore e;
+  e ← Meta.whnfCore e;
   condM (pred e)
     (do
-      e? ← unfoldDefinition? e;
+      e? ← Meta.unfoldDefinition? e;
       match e? with
       | some e => whnfHeadPredAux e
       | none   => pure e)
     (pure e)
 
-def whnfHeadPred (e : Expr) (pred : Expr → MetaM Bool) : MetaM Expr :=
-whnfHeadPredAux pred e
+end Meta
 
-def whnfUntil (e : Expr) (declName : Name) : MetaM (Option Expr) := do
-e ← whnfHeadPredAux (fun e => pure $ !e.isAppOf declName) e;
+section Methods
+variables {m : Type → Type} [MonadMetaM m]
+
+@[inline] def isAuxDef? (constName : Name) : m Bool :=
+liftMetaM $ Meta.isAuxDef? constName
+
+@[inline] def unfoldDefinition? (e : Expr) : m (Option Expr) :=
+liftMetaM $ Meta.unfoldDefinition? e
+
+@[inline] def whnfCore (e : Expr) : m Expr :=
+liftMetaM $ Meta.whnfCore e
+
+@[inline] def whnfHeadPred (e : Expr) (pred : Expr → MetaM Bool) : m Expr :=
+liftMetaM $ Meta.whnfHeadPredAux pred e
+
+def whnfUntil {m} [MonadMetaM m] (e : Expr) (declName : Name) : m (Option Expr) := liftMetaM do
+e ← Meta.whnfHeadPredAux (fun e => pure $ !e.isAppOf declName) e;
 if e.isAppOf declName then pure e
 else pure none
 
-def getStuckMVar? (e : Expr) : MetaM (Option MVarId) :=
-WHNF.getStuckMVar? getConst? whnf e
+def getStuckMVar? {m} [MonadMetaM m] (e : Expr) : m (Option MVarId) := liftMetaM do
+WHNF.getStuckMVar? Meta.getConst? whnf e
 
-end Meta
+end Methods
 end Lean
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index bd7bdee3f3..7db4a969a0 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -36,7 +36,7 @@ open Meta
 partial def compileParserBody {α} (ctx : Context α) : Expr → MetaM Expr | e => do
 e ← whnfCore e;
 match e with
-| e@(Expr.lam _ _ _ _)     => Meta.lambdaTelescope e fun xs b => compileParserBody b >>= Meta.mkLambda xs
+| e@(Expr.lam _ _ _ _)     => Meta.lambdaTelescope e fun xs b => compileParserBody b >>= mkLambdaFVars xs
 | e@(Expr.fvar _ _)        => pure e
 | _ => do
   let fn := e.getAppFn;
@@ -88,7 +88,7 @@ match e with
     else do
       -- if this is a generic function, e.g. `HasAndthen.andthen`, it's easier to just unfold it until we are
       -- back to parser combinators
-      some e' ← liftM $ unfoldDefinition? e
+      some e' ← unfoldDefinition? e
         | throwError $ "don't know how to generate " ++ ctx.varName ++ " for non-parser combinator '" ++ toString e ++ "'";
       compileParserBody e'
 end
diff --git a/src/Lean/Util/Closure.lean b/src/Lean/Util/Closure.lean
index 7bdf5b8279..a1f970b549 100644
--- a/src/Lean/Util/Closure.lean
+++ b/src/Lean/Util/Closure.lean
@@ -194,7 +194,7 @@ match (mkTypeValue { lctxInput := lctx, zeta := zeta }).run { mctx := mctx } wit
 
 end Closure
 
-def mkAuxDefinition (env : Environment) (opts : Options) (mctx : MetavarContext) (lctx : LocalContext) (name : Name) (type : Expr) (value : Expr)
+def mkAuxDefinitionCore (env : Environment) (opts : Options) (mctx : MetavarContext) (lctx : LocalContext) (name : Name) (type : Expr) (value : Expr)
     (zeta : Bool := false) : Except KernelException (Expr × Environment × MetavarContext) :=
 match Closure.mkClosure mctx lctx type value zeta with
 | Except.error ex  => throw $ KernelException.other ex