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

chore(library,hott): enforce naming conventions

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-17 11:36:35 -08:00
parent 13419d1561
commit c824a0e050
6 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/init/tactic.hlean
View file

@ -117,7 +117,7 @@ definition change (e : expr) : tactic := builtin
definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
definition notetac (id : identifier) (e : expr) : tactic := builtin
definition note_tac (id : identifier) (e : expr) : tactic := builtin
definition constructor (k : option num) : tactic := builtin
definition fconstructor (k : option num) : tactic := builtin

2
library/init/tactic.lean
View file

@ -121,7 +121,7 @@ definition change (e : expr) : tactic := builtin
definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
definition notetac (id : identifier) (e : expr) : tactic := builtin
definition note_tac (id : identifier) (e : expr) : tactic := builtin
definition constructor (k : option num) : tactic := builtin
definition fconstructor (k : option num) : tactic := builtin

8
src/library/constants.cpp
View file

@ -230,7 +230,7 @@ name const * g_tactic_interleave = nullptr;
name const * g_tactic_intro = nullptr;
name const * g_tactic_intros = nullptr;
name const * g_tactic_none_expr = nullptr;
name const * g_tactic_notetac = nullptr;
name const * g_tactic_note_tac = nullptr;
name const * g_tactic_now = nullptr;
name const * g_tactic_opt_expr = nullptr;
name const * g_tactic_opt_expr_list = nullptr;
@ -488,7 +488,7 @@ void initialize_constants() {
g_tactic_intro = new name{"tactic", "intro"};
g_tactic_intros = new name{"tactic", "intros"};
g_tactic_none_expr = new name{"tactic", "none_expr"};
g_tactic_notetac = new name{"tactic", "notetac"};
g_tactic_note_tac = new name{"tactic", "note_tac"};
g_tactic_now = new name{"tactic", "now"};
g_tactic_opt_expr = new name{"tactic", "opt_expr"};
g_tactic_opt_expr_list = new name{"tactic", "opt_expr_list"};
@ -747,7 +747,7 @@ void finalize_constants() {
delete g_tactic_intro;
delete g_tactic_intros;
delete g_tactic_none_expr;
delete g_tactic_notetac;
delete g_tactic_note_tac;
delete g_tactic_now;
delete g_tactic_opt_expr;
delete g_tactic_opt_expr_list;
@ -1005,7 +1005,7 @@ name const & get_tactic_interleave_name() { return *g_tactic_interleave; }
name const & get_tactic_intro_name() { return *g_tactic_intro; }
name const & get_tactic_intros_name() { return *g_tactic_intros; }
name const & get_tactic_none_expr_name() { return *g_tactic_none_expr; }
name const & get_tactic_notetac_name() { return *g_tactic_notetac; }
name const & get_tactic_note_tac_name() { return *g_tactic_note_tac; }
name const & get_tactic_now_name() { return *g_tactic_now; }
name const & get_tactic_opt_expr_name() { return *g_tactic_opt_expr; }
name const & get_tactic_opt_expr_list_name() { return *g_tactic_opt_expr_list; }

2
src/library/constants.h
View file

@ -232,7 +232,7 @@ name const & get_tactic_interleave_name();
name const & get_tactic_intro_name();
name const & get_tactic_intros_name();
name const & get_tactic_none_expr_name();
name const & get_tactic_notetac_name();
name const & get_tactic_note_tac_name();
name const & get_tactic_now_name();
name const & get_tactic_opt_expr_name();
name const & get_tactic_opt_expr_list_name();

2
src/library/constants.txt
View file

@ -225,7 +225,7 @@ tactic.interleave
tactic.intro
tactic.intros
tactic.none_expr
tactic.notetac
tactic.note_tac
tactic.now
tactic.opt_expr
tactic.opt_expr_list

4
src/library/tactic/note_tactic.cpp
View file

@ -14,7 +14,7 @@ Author: Leonardo de Moura
namespace lean {
expr mk_note_tactic_expr(name const &id, expr const &e) {
return mk_app(mk_constant(get_tactic_notetac_name()),
return mk_app(mk_constant(get_tactic_note_tac_name()),
mk_constant(id), e);
}
@ -51,7 +51,7 @@ tactic note_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
}
void initialize_note_tactic() {
register_tac(get_tactic_notetac_name(),
register_tac(get_tactic_note_tac_name(),
[](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'note' tactic, argument must be an identifier");
check_tactic_expr(app_arg(e), "invalid 'note' tactic, argument must be an expression");