diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 37d6250b39..29b204976f 100755
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -352,6 +352,7 @@ void pretty_fn::set_options_core(options const & _o) {
     m_hide_comp_irrel   = get_pp_hide_comp_irrel(o);
     m_delayed_abstraction  = get_pp_delayed_abstraction(o);
     m_use_holes         = get_pp_use_holes(o);
+    m_annotations       = get_pp_annotations(o);
     m_hide_full_terms   = get_formatter_hide_full_terms(o);
     m_num_nat_coe       = m_numerals;
     m_structure_instances = get_pp_structure_instances(o);
@@ -1191,7 +1192,10 @@ auto pretty_fn::pp_macro(expr const & e) -> result {
         else
             return pp_macro_default(e);
     } else if (is_annotation(e)) {
-        return pp(get_annotation_arg(e));
+        if (m_annotations)
+            return format("[") + format(get_annotation_kind(e)) + space() + pp(get_annotation_arg(e)).fmt() + format("]");
+        else
+            return pp(get_annotation_arg(e));
     } else if (is_rec_fn_macro(e)) {
         return format("[") + format(get_rec_fn_name(e)) + format("]");
     } else if (is_synthetic_sorry(e)) {
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index 14227a43a6..38f7351545 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -79,6 +79,7 @@ private:
     bool                    m_structure_instances_qualifier;
     bool                    m_structure_projections;
     bool                    m_use_holes;
+    bool                    m_annotations;
 
     name mk_metavar_name(name const & m, optional<name> const & prefix = optional<name>());
     name mk_metavar_name(name const & m, name const & prefix) {
diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp
index 3d92e97f44..740540bf18 100644
--- a/src/library/pp_options.cpp
+++ b/src/library/pp_options.cpp
@@ -116,6 +116,10 @@ Author: Leonardo de Moura
 #define LEAN_DEFAULT_PP_USE_HOLES false
 #endif
 
+#ifndef LEAN_DEFAULT_PP_ANNOTATIONS
+#define LEAN_DEFAULT_PP_ANNOTATIONS false
+#endif
+
 namespace lean {
 static name * g_pp_max_depth         = nullptr;
 static name * g_pp_max_steps         = nullptr;
@@ -143,6 +147,7 @@ static name * g_pp_structure_instances_qualifier = nullptr;
 static name * g_pp_structure_projections    = nullptr;
 static name * g_pp_instantiate_mvars = nullptr;
 static name * g_pp_use_holes         = nullptr;
+static name * g_pp_annotations       = nullptr;
 static name * g_pp_all               = nullptr;
 static list<options> * g_distinguishing_pp_options = nullptr;
 
@@ -174,6 +179,7 @@ void initialize_pp_options() {
     g_pp_structure_projections = new name{"pp", "structure_projections"};
     g_pp_instantiate_mvars = new name{"pp", "instantiate_mvars"};
     g_pp_use_holes         = new name{"pp", "use_holes"};
+    g_pp_annotations       = new name{"pp", "annotations"};
 
     register_unsigned_option(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH,
                              "(pretty printer) maximum expression depth, after that it will use ellipsis");
@@ -235,6 +241,8 @@ void initialize_pp_options() {
                          "(pretty printer) instantiate assigned metavariables before pretty printing terms and goals");
     register_bool_option(*g_pp_use_holes, LEAN_DEFAULT_PP_USE_HOLES,
                          "(pretty printer) use holes '{! !}' when pretty printing metavariables and `sorry`");
+    register_bool_option(*g_pp_annotations, LEAN_DEFAULT_PP_ANNOTATIONS,
+                         "(pretty printer) display internal annotations (for debugging purposes only)");
 
     options universes_true(*g_pp_universes, true);
     options full_names_true(*g_pp_full_names, true);
@@ -280,6 +288,7 @@ void finalize_pp_options() {
     delete g_pp_delayed_abstraction;
     delete g_pp_instantiate_mvars;
     delete g_pp_use_holes;
+    delete g_pp_annotations;
     delete g_distinguishing_pp_options;
 }
 
@@ -325,5 +334,6 @@ bool     get_pp_structure_instances_qualifier(options const & opts) { return opt
 bool     get_pp_structure_projections(options const & opts) { return opts.get_bool(*g_pp_structure_projections, LEAN_DEFAULT_PP_STRUCTURE_PROJECTIONS); }
 bool     get_pp_instantiate_mvars(options const & o)    { return o.get_bool(*g_pp_instantiate_mvars, LEAN_DEFAULT_PP_INSTANTIATE_MVARS); }
 bool     get_pp_use_holes(options const & o)            { return o.get_bool(*g_pp_use_holes, LEAN_DEFAULT_PP_USE_HOLES); }
+bool     get_pp_annotations(options const & o)          { return o.get_bool(*g_pp_annotations, LEAN_DEFAULT_PP_ANNOTATIONS); }
 bool     get_pp_all(options const & opts)               { return opts.get_bool(*g_pp_all, LEAN_DEFAULT_PP_ALL); }
 }
diff --git a/src/library/pp_options.h b/src/library/pp_options.h
index c4da9d8434..38b3388ecd 100644
--- a/src/library/pp_options.h
+++ b/src/library/pp_options.h
@@ -49,6 +49,7 @@ bool     get_pp_structure_instances_qualifier(options const & opts);
 bool     get_pp_structure_projections(options const & opts);
 bool     get_pp_instantiate_mvars(options const & o);
 bool     get_pp_use_holes(options const & o);
+bool     get_pp_annotations(options const & o);
 bool     get_pp_all(options const & opts);
 
 void initialize_pp_options();