diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index c699c873c..8fdff1ea0 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -29,6 +29,7 @@ Author: Leonardo de Moura
 #include "library/pp_options.h"
 #include "library/constants.h"
 #include "library/replace_visitor.h"
+#include "library/definitional/equations.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/token_table.h"
@@ -672,6 +673,10 @@ auto pretty_fn::pp_explicit(expr const & e) -> result {
 auto pretty_fn::pp_macro(expr const & e) -> result {
     if (is_explicit(e)) {
         return pp_explicit(e);
+    } else if (is_inaccessible(e)) {
+        format li = m_unicode ? format("⌞") : format("?(");
+        format ri = m_unicode ? format("⌟") : format(")");
+        return result(group(nest(1, li + pp(get_annotation_arg(e)).fmt() + ri)));
     } else if (is_annotation(e)) {
         return pp(get_annotation_arg(e));
     } else {