From 17e3223467510faee90848bcab369e50b96f36b7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 May 2016 14:14:43 -0700
Subject: [PATCH] chore(library/vm/vm): add debugging helper procedure

---
 src/library/vm/vm.cpp | 5 +++++
 1 file changed, 5 insertions(+)

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";
+}