diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index e43959ab4..e37440f6d 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -54,7 +54,7 @@ public: set('\'', 'a'); // characters that can be used to create ids of group b - for (unsigned char b : {'=', '<', '>', '@', '^', '|', '&', '~', '+', '-', '*', '/', '\\', '$', '%', '?', ';', '[', ']'}) + for (unsigned char b : {'=', '<', '>', '@', '^', '|', '&', '~', '+', '-', '*', '/', '\\', '$', '%', '?', ';', '[', ']', '#'}) set(b, 'b'); // punctuation