feat(frontends/lean): add notation for providing patterns

src/frontends/lean/builtin_exprs.cpp

@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/definitional/equations.h"
 #include "library/tactic/assert_tactic.h"
+#include "library/blast/forward/pattern.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/token_table.h"
@@ -737,6 +738,10 @@ static expr parse_typed_expr(parser & p, unsigned, expr const * args, pos_info c
     return mk_typed_expr_distrib_choice(p, args[1], args[0], pos);
 }
 
+static expr parse_pattern(parser & p, unsigned, expr const * args, pos_info const & pos) {
+    return p.save_pos(mk_pattern(args[0]), pos);
+}
+
 parse_table init_nud_table() {
     action Expr(mk_expr_action());
     action Skip(mk_skip_action());
@@ -758,6 +763,7 @@ parse_table init_nud_table() {
     r = r.add({transition("(", Expr), transition(":", Expr), transition(")", mk_ext_action(parse_typed_expr))}, x0);
     r = r.add({transition("?(", Expr), transition(")", mk_ext_action(parse_inaccessible))}, x0);
     r = r.add({transition("⌞", Expr), transition("⌟", mk_ext_action(parse_inaccessible))}, x0);
+    r = r.add({transition("(:", Expr), transition(":)", mk_ext_action(parse_pattern))}, x0);
     r = r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0);
     r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0);
     r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0);

src/frontends/lean/pp.cpp

@@ -33,6 +33,7 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/replace_visitor.h"
 #include "library/definitional/equations.h"
+#include "library/blast/forward/pattern.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/token_table.h"
@@ -794,6 +795,8 @@ auto pretty_fn::pp_macro(expr const & e) -> result {
         format li = m_unicode ? format("⌞") : format("?(");
         format ri = m_unicode ? format("⌟") : format(")");
         return result(group(nest(1, li + pp(get_annotation_arg(e)).fmt() + ri)));
+    } else if (is_pattern(e)) {
+        return result(group(nest(2, format("(:") + pp(get_pattern_arg(e)).fmt() + format(":)"))));
     } else if (is_annotation(e)) {
         return pp(get_annotation_arg(e));
     } else {

src/frontends/lean/token_table.cpp

@@ -92,7 +92,8 @@ void init_token_table(token_table & t) {
          {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"by+", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},
-         {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
+         {"{|", g_max_prec}, {"|}", 0}, {"(:", g_max_prec}, {":)", 0},
+         {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
          {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0},
          {"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"with_options", 0}, {"simp", 0},