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

feat(library/app_builder): add set_context

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-01 12:12:41 -08:00
parent 137ec27059
commit b5c40e30ef
2 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/app_builder.cpp
View file

@ -226,4 +226,8 @@ optional<expr> app_builder::mk_app(name const & c, unsigned nargs, expr const *
optional<expr> app_builder::mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args) { optional<expr> app_builder::mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args) {
return m_ptr->mk_app(c, mask_sz, mask, args); return m_ptr->mk_app(c, mask_sz, mask, args);
} }
void app_builder::set_context(list<expr> const & ctx) {
m_ptr->m_ctx->set_context(ctx);
}
} }

7
src/library/app_builder.h
View file

@ -62,5 +62,12 @@ public:
} }
optional<expr> mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args); optional<expr> mk_app(name const & c, unsigned mask_sz, bool const * mask, expr const * args);
/** \brief Set the local context. This method is relevant when we want to expose local class instances
to the app_builder.
\remark When the constructor app_builder(std::unique_ptr<tmp_type_context> && ctx) is used
the initialization can be performed outside. */
void set_context(list<expr> const & ctx);
}; };
} }