diff --git a/src/library/vm.cpp b/src/library/vm.cpp
index dff0aa277a..b0e4becc7f 100644
--- a/src/library/vm.cpp
+++ b/src/library/vm.cpp
@@ -491,6 +491,14 @@ environment optimize_vm_decls(environment const & env) {
     }
 }
 
+optional<vm_decl> get_vm_decl(environment const & env, name const & n) {
+    vm_decls const & ext = get_extension(env);
+    if (auto idx = ext.m_name2idx.find(n))
+        return optional<vm_decl>(ext.m_decls[*idx]);
+    else
+        return optional<vm_decl>();
+}
+
 vm_state::vm_state(environment const & env):
     m_env(optimize_vm_decls(env)),
     m_decls(get_extension(m_env).m_decls.as_vector_if_compressed()),
diff --git a/src/library/vm.h b/src/library/vm.h
index d02ea4f30a..dd399184b9 100644
--- a/src/library/vm.h
+++ b/src/library/vm.h
@@ -424,6 +424,8 @@ bool is_vm_function(environment const & env, name const & fn);
 /** \brief Return true iff \c fn is implemented in C++. */
 bool is_vm_builtin_function(name const & fn);
 
+optional<vm_decl> get_vm_decl(environment const & env, name const & n);
+
 void display_vm_code(std::ostream & out, environment const & env, unsigned code_sz, vm_instr const * code);
 
 void initialize_vm();