From ac7b70c555985f84cc9792c1402ca72b4ef10cc0 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 25 Sep 2018 12:20:08 -0700 Subject: [PATCH] fix(frontends/lean/token_table): add missing built-in token `::` is used not only by `list` but also the built-in `structure` command --- src/frontends/lean/token_table.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index ad2ef93637..7a1d1c2097 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -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[] =