diff --git a/src/library/vm.cpp b/src/library/vm.cpp index fad26efd8f..7528076f38 100644 --- a/src/library/vm.cpp +++ b/src/library/vm.cpp @@ -342,6 +342,10 @@ void declare_vm_builtin(name const & n, unsigned arity, vm_function fn) { g_vm_builtins->insert(n, mk_pair(arity, fn)); } +bool is_vm_builtin_function(name const & fn) { + return g_vm_builtins->contains(fn); +} + /** \brief VM function/constant declarations are stored in an environment extension. */ struct vm_decls : public environment_extension { bool m_initialized; diff --git a/src/library/vm.h b/src/library/vm.h index be5cbaf554..80063c6502 100644 --- a/src/library/vm.h +++ b/src/library/vm.h @@ -341,6 +341,9 @@ environment optimize_vm_decls(environment const & env); /** \brief Return true iff \c fn is a VM function in the given environment. */ 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); + void initialize_vm(); void finalize_vm(); }