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

chore(frontends/lean): remove 'dead' tokens

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-05 14:28:10 -08:00
parent b73a931c70
commit 8e9ccf8b6f
3 changed files with 1 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/token_table.cpp
View file

@ -90,7 +90,7 @@ void init_token_table(token_table & t) {
{"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
"abbreviation",
"variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
"[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
"[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
"[parsing-only]", "[multiple-instances]",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-c", "print",
"end", "namespace", "section", "prelude",

8
src/frontends/lean/tokens.cpp
View file

@ -68,8 +68,6 @@ static name * g_exposing = nullptr;
static name * g_renaming = nullptr;
static name * g_extends = nullptr;
static name * g_as = nullptr;
static name * g_on = nullptr;
static name * g_off = nullptr;
static name * g_none = nullptr;
static name * g_whnf = nullptr;
static name * g_wf = nullptr;
@ -190,8 +188,6 @@ void initialize_tokens() {
g_renaming = new name("renaming");
g_extends = new name("extends");
g_as = new name("as");
g_on = new name("[on]");
g_off = new name("[off]");
g_none = new name("[none]");
g_whnf = new name("[whnf]");
g_wf = new name("[wf]");
@ -320,8 +316,6 @@ void finalize_tokens() {
delete g_renaming;
delete g_extends;
delete g_as;
delete g_on;
delete g_off;
delete g_none;
delete g_whnf;
delete g_wf;
@ -436,8 +430,6 @@ name const & get_exposing_tk() { return *g_exposing; }
name const & get_renaming_tk() { return *g_renaming; }
name const & get_extends_tk() { return *g_extends; }
name const & get_as_tk() { return *g_as; }
name const & get_on_tk() { return *g_on; }
name const & get_off_tk() { return *g_off; }
name const & get_none_tk() { return *g_none; }
name const & get_whnf_tk() { return *g_whnf; }
name const & get_wf_tk() { return *g_wf; }

2
src/frontends/lean/tokens.h
View file

@ -70,8 +70,6 @@ name const & get_exposing_tk();
name const & get_renaming_tk();
name const & get_extends_tk();
name const & get_as_tk();
name const & get_on_tk();
name const & get_off_tk();
name const & get_none_tk();
name const & get_whnf_tk();
name const & get_wf_tk();