chore(library/vm/vm): add debugging helper procedure

This commit is contained in:
Leonardo de Moura 2016-05-23 14:14:43 -07:00
parent 9545620a54
commit 17e3223467

View file

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