diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index 8396036296..53820e415b 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -607,6 +607,14 @@ forallTelescopeReducingAux isClassExpensive type none k
 def forallBoundedTelescope {α} (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → MetaM α) : MetaM α :=
 forallTelescopeReducingAux isClassExpensive type maxFVars? k
 
+/-- Return the parameter names for the givel global declaration. -/
+def getParamNames (declName : Name) : MetaM (Array Name) := do
+cinfo ← getConstInfo declName;
+forallTelescopeReducing cinfo.type $ fun xs _ => do
+  xs.mapM $ fun x => do
+    localDecl ← getLocalDecl x.fvarId!;
+    pure localDecl.userName
+
 def isClass (type : Expr) : MetaM (Option Name) := do
 c? ← isClassQuick type;
 match c? with
diff --git a/tests/lean/run/meta5.lean b/tests/lean/run/meta5.lean
new file mode 100644
index 0000000000..394e58137f
--- /dev/null
+++ b/tests/lean/run/meta5.lean
@@ -0,0 +1,26 @@
+import Init.Lean.Meta
+open Lean
+open Lean.Meta
+
+def tst1 : MetaM Unit :=
+withLocalDecl `y (mkConst `Nat) BinderInfo.default $ fun y => do
+withLetDecl `x (mkConst `Nat) (mkNatLit 0) $ fun x => do {
+  mvar ← mkFreshExprMVar (mkConst `Nat) Name.anonymous MetavarKind.syntheticOpaque;
+  trace! `Meta mvar;
+  r ← mkLambda #[y, x] mvar;
+  trace! `Meta r;
+  let v := mkApp2 (mkConst `Nat.add) x y;
+  assignExprMVar mvar.mvarId! v;
+  trace! `Meta mvar;
+  trace! `Meta r;
+  mctx ← getMCtx;
+  mctx.decls.forM $ fun mvarId mvarDecl => do {
+    trace! `Meta ("?" ++ mvarId ++ " : " ++ mvarDecl.type);
+    pure ()
+  };
+  pure ()
+}
+
+set_option trace.Meta true
+
+#eval tst1
diff --git a/tests/lean/run/meta6.lean b/tests/lean/run/meta6.lean
new file mode 100644
index 0000000000..f2bff8b6ba
--- /dev/null
+++ b/tests/lean/run/meta6.lean
@@ -0,0 +1,43 @@
+import Init.Lean.Meta
+open Lean
+open Lean.Meta
+
+def print (msg : MessageData) : MetaM Unit :=
+trace! `Meta.debug msg
+
+def check (x : MetaM Bool) : MetaM Unit :=
+unlessM x $ throw $ Exception.other "check failed"
+
+def nat   := mkConst `Nat
+def boolE := mkConst `Bool
+def succ  := mkConst `Nat.succ
+def zero  := mkConst `Nat.zero
+def add   := mkConst `Nat.add
+def io    := mkConst `IO
+def type  := mkSort levelOne
+def mkArrow (d b : Expr) : Expr := mkForall `_ BinderInfo.default d b
+
+def tst1 : MetaM Unit := do
+print "----- tst1 -----";
+m1 ← mkFreshExprMVar (mkArrow nat nat);
+let lhs := mkApp m1 zero;
+let rhs := zero;
+check $ approxDefEq $ isDefEq lhs rhs;
+pure ()
+
+set_option pp.all true
+set_option trace.Meta.isDefEq true
+
+#eval tst1
+
+set_option trace.Meta true
+set_option trace.Meta.isDefEq false
+
+def tst2 : MetaM Unit := do
+print "----- tst2 -----";
+ps ← getParamNames `Or.elim; print (toString ps);
+ps ← getParamNames `Iff.elim; print (toString ps);
+ps ← getParamNames `check; print (toString ps);
+pure ()
+
+#eval tst2