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

fix(frontends/lean): remove keywords 'class' and '[class]'

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-30 15:05:44 -07:00
parent 9637ceb86e
commit 1d62a614e7
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -73,12 +73,12 @@ token_table init_token_table() {
{"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion", char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion",
"variables", "[private]", "[inline]", "[fact]", "[instance]", "[class]", "[module]", "[coercion]", "variables", "[private]", "[inline]", "[fact]", "[instance]", "[module]", "[coercion]",
"abbreviation", "opaque_hint", "evaluate", "check", "print", "end", "namespace", "section", "import", "abbreviation", "opaque_hint", "evaluate", "check", "print", "end", "namespace", "section", "import",
"abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe", "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe",
"precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
"exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans", "tactic_hint", "exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans", "tactic_hint",
"add_proof_qed", "set_proof_qed", "#setline", "class", "instance", nullptr}; "add_proof_qed", "set_proof_qed", "#setline", "instance", nullptr};
std::pair<char const *, char const *> aliases[] = std::pair<char const *, char const *> aliases[] =
{{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},