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

fix(frontends/lean/token_table): add missing built-in token

Browse source 
`::` is used not only by `list` but also the built-in `structure` command
This commit is contained in:
Sebastian Ullrich 2018-09-25 12:20:08 -07:00
parent 95c469f8c4
commit ac7b70c555
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

@ -96,7 +96,7 @@ void init_token_table(token_table & t) {
{"/-", 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},
{"match", 0}, {"^.", g_max_prec+1},
{"match", 0}, {"^.", g_max_prec+1}, {"::", 67},
{"renaming", 0}, {"extends", 0}, {"node!", g_max_prec}, {"node_choice!", g_max_prec}, {nullptr, 0}};
char const * commands[] =