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

feat(library/tactic/tactic_state): add tactic mk_fresh_name

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-18 13:02:45 -07:00
parent bf5cf18d8d
commit b546167a64
2 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -146,7 +146,7 @@ meta_constant get_univ_assignment : level → tactic level
/- Return the value assigned to the given meta-variable.
Fail if argument is not a meta-variable or if it is not assigned. -/
meta_constant get_assignment : expr → tactic expr
meta_constant mk_fresh_name : tactic name
open list nat
meta_definition intros : tactic unit :=

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

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/fresh_name.h"
#include "library/constants.h"
#include "library/type_context.h"
#include "library/pp_options.h"
@ -462,6 +463,10 @@ vm_obj tactic_state_set_options(vm_obj const & s, vm_obj const & o) {
return to_obj(set_options(to_tactic_state(s), to_options(o)));
}
vm_obj tactic_mk_fresh_name(vm_obj const & s) {
return mk_tactic_success(to_obj(mk_fresh_name()), 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);
@ -487,6 +492,7 @@ void initialize_tactic_state() {
DECLARE_VM_BUILTIN(name({"tactic", "mk_meta_var"}), tactic_mk_meta_var);
DECLARE_VM_BUILTIN(name({"tactic", "get_univ_assignment"}), tactic_get_univ_assignment);
DECLARE_VM_BUILTIN(name({"tactic", "get_assignment"}), tactic_get_assignment);
DECLARE_VM_BUILTIN(name({"tactic", "mk_fresh_name"}), tactic_mk_fresh_name);
}
void finalize_tactic_state() {