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

chore(frontends/lean/token_table): remove 'note' keyword

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-20 11:01:20 -07:00
parent d03dc18096
commit 149fefe480
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -97,7 +97,7 @@ void init_token_table(token_table & t) {
{"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
{"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0},
{".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0},
{"esimp", 0}, {"note", 0}, {"with_options", 0}, {"with_attributes", 0}, {"with_attrs", 0},
{"esimp", 0}, {"with_options", 0}, {"with_attributes", 0}, {"with_attrs", 0},
{"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"#tactic", 0},
{"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec},
{"@@", g_max_prec}, {"@", g_max_prec},