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

feat(library/init/meta/tactic): add tactic.opened_namespaces

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-18 14:25:54 -08:00
parent 6d06f8bf29
commit 2844df2279
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/tactic.lean
View file

@ -364,6 +364,8 @@ try $ do
/- (save_type_info e ref) save (typeof e) at position associated with ref -/
meta constant save_type_info : expr → expr → tactic unit
/- Return list of currently opened namespace -/
meta constant opened_namespaces : tactic (list name)
open list nat
/- Remark: set_goals will erase any solved goal -/

7
src/library/tactic/tactic_state.cpp
View file

@ -15,6 +15,7 @@ Author: Leonardo de Moura
#include "library/util.h"
#include "library/cache_helper.h"
#include "library/module.h"
#include "library/scoped_ext.h"
#include "library/vm/vm_environment.h"
#include "library/vm/vm_exceptional.h"
#include "library/vm/vm_format.h"
@ -613,6 +614,11 @@ vm_obj tactic_add_decl(vm_obj const & _d, vm_obj const & _s) {
}
}
vm_obj tactic_opened_namespaces(vm_obj const & s) {
environment env = to_tactic_state(s).env();
return mk_tactic_success(to_obj(get_namespaces(env)), to_tactic_state(s));
}
void initialize_tactic_state() {
DECLARE_VM_BUILTIN(name({"tactic_state", "env"}), tactic_state_env);
DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}), tactic_state_format_expr);
@ -645,6 +651,7 @@ void initialize_tactic_state() {
DECLARE_VM_BUILTIN(name({"tactic", "is_trace_enabled_for"}), tactic_is_trace_enabled_for);
DECLARE_VM_BUILTIN(name({"tactic", "instantiate_mvars"}), tactic_instantiate_mvars);
DECLARE_VM_BUILTIN(name({"tactic", "add_decl"}), tactic_add_decl);
DECLARE_VM_BUILTIN(name({"tactic", "opened_namespaces"}), tactic_opened_namespaces);
g_pp_instantiate_goal_mvars = new name{"pp", "instantiate_goal_mvars"};
register_bool_option(*g_pp_instantiate_goal_mvars, LEAN_DEFAULT_PP_INSTANTIATE_GOAL_MVARS,
"(pretty printer) instantiate assigned metavariables before pretty printing goals");