diff --git a/src/frontends/lean/operator_info.cpp b/src/frontends/lean/operator_info.cpp
index 39dcd8d209..b96c788ae6 100644
--- a/src/frontends/lean/operator_info.cpp
+++ b/src/frontends/lean/operator_info.cpp
@@ -183,4 +183,14 @@ std::ostream & operator<<(std::ostream & out, operator_info const & o) {
     out << pp(o);
     return out;
 }
+
+regular const & operator<<(regular const & out, operator_info const & o) {
+    out.m_io_state.get_regular_channel().get_stream() << mk_pair(pp(o), out.m_io_state.get_options());
+    return out;
+}
+
+diagnostic const & operator<<(diagnostic const & out, operator_info const & o) {
+    out.m_io_state.get_diagnostic_channel().get_stream() << mk_pair(pp(o), out.m_io_state.get_options());
+    return out;
+}
 }
diff --git a/src/frontends/lean/operator_info.h b/src/frontends/lean/operator_info.h
index 3daef1d301..712328e287 100644
--- a/src/frontends/lean/operator_info.h
+++ b/src/frontends/lean/operator_info.h
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "util/name.h"
 #include "util/list.h"
 #include "util/sexpr/format.h"
+#include "library/io_state.h"
 #include "kernel/object.h"
 
 namespace lean {
@@ -110,6 +111,9 @@ inline operator_info mixfixo(std::initializer_list<name> const & l, unsigned pre
 format pp(operator_info const & o);
 std::ostream & operator<<(std::ostream & out, operator_info const & o);
 
+regular const & operator<<(regular const & out, operator_info const & o);
+diagnostic const & operator<<(diagnostic const & out, operator_info const & o);
+
 /**
     \brief Create object for tracking notation/operator declarations.
     This object is mainly used for recording the declaration.