diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index 54bf46a6da..c70d21636b 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -1198,3 +1198,8 @@ void finalize_vm() {
     delete g_vm_code_key;
 }
 }
+
+void print(lean::vm_obj const & o) {
+    ::lean::display(std::cout, o);
+    std::cout << "\n";
+}