feat(frontends/lean/parser): allow string literals in patterns

library/init/char.lean

@@ -11,6 +11,7 @@ definition char := fin 256
 
 namespace char
 
+attribute [pattern]
 definition of_nat (n : nat) : char :=
 if H : n < 256 then fin.mk n H else fin.mk 0 dec_trivial
 

library/init/string.lean

@@ -10,7 +10,11 @@ attribute [reducible]
 definition string := list char
 
 namespace string
+
+attribute [pattern]
 definition empty : string := list.nil
+
+attribute [pattern]
 definition str : char → string → string := list.cons
 
 definition concat (a b : string) : string :=

src/frontends/lean/parser.cpp

@@ -1709,7 +1709,7 @@ struct to_pattern_fn {
     void collect_new_locals(expr const & e, bool skip_main_fn) {
         if (is_typed_expr(e)) {
             collect_new_locals(get_typed_expr_expr(e), false);
-        } else if (is_prenum(e)) {
+        } else if (is_prenum(e) || is_string_macro(e)) {
             // do nothing
         } else if (is_inaccessible(e)) {
             // do nothing
@@ -1754,7 +1754,7 @@ struct to_pattern_fn {
             expr new_v = visit(get_typed_expr_expr(e));
             expr new_t = to_expr(get_typed_expr_type(e));
             return copy_tag(e, mk_typed_expr(new_t, new_v));
-        } else if (is_prenum(e)) {
+        } else if (is_prenum(e) || is_string_macro(e)) {
             return e;
         } else if (is_inaccessible(e)) {
             return to_expr(e);

src/library/string.h

@@ -17,6 +17,8 @@ expr from_string(std::string const & s);
     \see from_string */
 optional<std::string> to_string(expr const & e);
 
+bool is_string_macro(expr const & e);
+
 optional<char> to_char(expr const & e);
 
 format pp_string_literal(std::string const & s);