feat(library/vm): add is_vm_builtin_function

This commit is contained in:
Leonardo de Moura 2016-05-11 12:49:54 -07:00
parent 74b9690b7f
commit 53308d55b1
2 changed files with 7 additions and 0 deletions

View file

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

View file

@ -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();
}