michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/module): add extra function for adding uncertified declarations when trust_lvl > LEAN_BELIEVER_TRUST_LEVEL

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-23 10:50:34 -07:00
parent a0a70bcea7
commit 1a663afda4
2 changed files with 12 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/module.cpp
View file

@ -129,8 +129,13 @@ static register_module_object_reader_fn g_reg_decl_reader(g_decl, declaration_re
environment add(environment const & env, certified_declaration const & d) { environment add(environment const & env, certified_declaration const & d) {
environment new_env = env.add(d); environment new_env = env.add(d);
new_env = add(new_env, g_decl, [=](serializer & s) { s << d.get_declaration(); }); declaration _d = d.get_declaration();
return new_env; return add(new_env, g_decl, [=](serializer & s) { s << _d; });
}
environment add(environment const & env, declaration const & d) {
environment new_env = env.add(d);
return add(new_env, g_decl, [=](serializer & s) { s << d; });
} }
struct import_modules_fn { struct import_modules_fn {

5
src/library/module.h
View file

@ -70,4 +70,9 @@ environment add(environment const & env, std::string const & k, std::function<vo
/** \brief Add the given declaration to the environment, and mark it to be exported. */ /** \brief Add the given declaration to the environment, and mark it to be exported. */
environment add(environment const & env, certified_declaration const & d); environment add(environment const & env, certified_declaration const & d);
/**
\brief Add the given declaration to the environment, and mark it to be exported.
This method throws an exception if the trust_level <= LEAN_BELIEVER_TRUST_LEVEL
*/
environment add(environment const & env, declaration const & d);
} }