diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 384fd1020..6750d8aea 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -113,6 +113,7 @@ void pretty_fn::set_options_core(options const & o) {
     m_universes     = get_pp_universes(o);
     m_full_names    = get_pp_full_names(o);
     m_private_names = get_pp_private_names(o);
+    m_metavar_args  = get_pp_metavar_args(o);
 }
 
 void pretty_fn::set_options(options const & o) {
@@ -412,6 +413,7 @@ auto pretty_fn::pp(expr const & e) -> result {
     if (is_show(e)) return pp_show(e);
     if (is_let(e))  return pp_let(e);
     if (is_have(e)) return pp_have(e);
+    if (!m_metavar_args && is_meta(e)) return pp_meta(get_app_fn(e));
 
     switch (e.kind()) {
     case expr_kind::Var:       return pp_var(e);
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index f8ce5de87..2ba812184 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -40,6 +40,7 @@ private:
     bool               m_universes;
     bool               m_full_names;
     bool               m_private_names;
+    bool               m_metavar_args;
 
     unsigned max_bp() const { return std::numeric_limits<unsigned>::max(); }
     name mk_metavar_name(name const & m);
diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp
index 2831ed21e..011f18ebe 100644
--- a/src/frontends/lean/pp_options.cpp
+++ b/src/frontends/lean/pp_options.cpp
@@ -38,6 +38,10 @@ Author: Leonardo de Moura
 #define LEAN_DEFAULT_PP_PRIVATE_NAMES false
 #endif
 
+#ifndef LEAN_DEFAULT_PP_METAVAR_ARGS
+#define LEAN_DEFAULT_PP_METAVAR_ARGS false
+#endif
+
 namespace lean {
 static name g_pp_max_depth        {"pp", "max_depth"};
 static name g_pp_max_steps        {"pp", "max_steps"};
@@ -47,6 +51,7 @@ static name g_pp_coercion         {"pp", "coercion"};
 static name g_pp_universes        {"pp", "universes"};
 static name g_pp_full_names       {"pp", "full_names"};
 static name g_pp_private_names    {"pp", "private_names"};
+static name g_pp_metavar_args     {"pp", "metavar_args"};
 
 list<options> const & get_distinguishing_pp_options() {
     static options g_universes_true(g_pp_universes, true);
@@ -76,6 +81,8 @@ RegisterBoolOption(g_pp_full_names,  LEAN_DEFAULT_PP_FULL_NAMES,
                    "(pretty printer) display fully qualified names");
 RegisterBoolOption(g_pp_private_names,  LEAN_DEFAULT_PP_PRIVATE_NAMES,
                    "(pretty printer) display internal names assigned to private declarations");
+RegisterBoolOption(g_pp_metavar_args,  LEAN_DEFAULT_PP_METAVAR_ARGS,
+                   "(pretty printer) display metavariable arguments");
 
 unsigned get_pp_max_depth(options const & opts)     { return opts.get_unsigned(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); }
 unsigned get_pp_max_steps(options const & opts)     { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
@@ -85,4 +92,5 @@ bool     get_pp_coercion(options const & opts)      { return opts.get_bool(g_pp_
 bool     get_pp_universes(options const & opts)     { return opts.get_bool(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); }
 bool     get_pp_full_names(options const & opts)    { return opts.get_bool(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); }
 bool     get_pp_private_names(options const & opts) { return opts.get_bool(g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); }
+bool     get_pp_metavar_args(options const & opts)  { return opts.get_bool(g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS); }
 }
diff --git a/src/frontends/lean/pp_options.h b/src/frontends/lean/pp_options.h
index 6c09e5cb1..eff7cb951 100644
--- a/src/frontends/lean/pp_options.h
+++ b/src/frontends/lean/pp_options.h
@@ -15,5 +15,6 @@ bool     get_pp_coercion(options const & opts);
 bool     get_pp_universes(options const & opts);
 bool     get_pp_full_names(options const & opts);
 bool     get_pp_private_names(options const & opts);
+bool     get_pp_metavar_args(options const & opts);
 list<options> const & get_distinguishing_pp_options();
 }