max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/noncomputable): mark all VM builtins as computable

Browse source
This commit is contained in:
Sebastian Ullrich 2018-08-15 09:09:37 -07:00 • committed by Leonardo de Moura
parent fd9bc9e15b
commit 6e3a6ff40f
1 changed files with 2 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/noncomputable.cpp
View file

@ -16,6 +16,7 @@ Author: Leonardo de Moura
#include "library/trace.h"
#include "library/quote.h"
#include "library/constants.h"
#include "library/vm/vm.h"
// TODO(Leo): move inline attribute declaration to library
#include "library/compiler/inliner.h"
namespace lean {
@ -62,17 +63,10 @@ struct noncomputable_modification : public modification {
}
};
// TODO(Leo): implement better support for extending this set of builtin constants
static bool is_builtin_extra(name const & n) {
return
n == get_io_core_name() ||
n == get_sorry_ax_name() ||
n == get_monad_io_impl_name() ||
n == get_monad_io_terminal_impl_name() ||
n == get_monad_io_file_system_impl_name() ||
n == get_monad_io_environment_impl_name() ||
n == get_monad_io_process_impl_name() ||
n == get_monad_io_random_impl_name();
is_vm_builtin_function(n);
}
static bool is_noncomputable(old_type_checker & tc, noncomputable_ext const & ext, name const & n) {