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

chore(frontends/lean/token_table): remove old keyword

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-05 08:46:23 -07:00
parent c9af4f53c7
commit 73ed9db161
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

@ -89,7 +89,7 @@ void init_token_table(token_table & t) {
{"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
{"//", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0}, {"with", 0}, {"without", 0}, {"...", 0}, {",", 0},
{".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0},
{"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec}, {"using", 0},
{"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"using", 0},
{"@@", g_max_prec}, {"@", g_max_prec},
{"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0},
{"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},