diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index ca50bf29f..db5cf668e 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -457,6 +457,10 @@ public: name_map local2href; return to_blast_expr_fn(m_env, m_curr_state, m_uvar2uref, m_mvar2meta_mref, local2href)(e); } + + app_builder & get_app_builder() { + return m_app_builder; + } }; LEAN_THREAD_PTR(blastenv, g_blastenv); @@ -477,6 +481,11 @@ io_state const & ios() { return g_blastenv->get_ios(); } +app_builder & get_app_builder() { + lean_assert(g_blastenv); + return g_blastenv->get_app_builder(); +} + state & curr_state() { lean_assert(g_blastenv); return g_blastenv->get_curr_state(); diff --git a/src/library/blast/blast.h b/src/library/blast/blast.h index cc2df029d..27145b4ed 100644 --- a/src/library/blast/blast.h +++ b/src/library/blast/blast.h @@ -22,6 +22,8 @@ namespace blast { environment const & env(); /** \brief Return the thread local io_state being used by the blast tactic. */ io_state const & ios(); +/** \brief Return reference to blast thread local app_builder */ +app_builder & get_app_builder(); /** \brief Return the thread local current state begin processed by the blast tactic. */ state & curr_state(); /** \brief Return a thread local fresh local constant. */