From fdea8aba100444a2fb3451262196ab4189f08e2d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Nov 2013 08:42:25 -0700 Subject: [PATCH] feat(frontends/lean/scanner): allow '#' to be used in class B identifiers Signed-off-by: Leonardo de Moura --- src/frontends/lean/scanner.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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