feat(frontends/lean): support for '@@' -- the partial explicit operator

src/frontends/lean/builtin_exprs.cpp

@@ -690,6 +690,10 @@ static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info con
     }
 }
 
+static expr parse_partial_explicit_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    throw parser_error("partial explicit expressions (@) not supported yet", p.pos());
+}
+
 static expr parse_consume_args_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
     expr e = p.parse_expr(get_Max_prec());
     if (is_choice(e)) {
@@ -753,6 +757,7 @@ parse_table init_nud_table() {
     r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0);
     r = r.add({transition("#", mk_ext_action(parse_override_notation))}, x0);
     r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0);
+    r = r.add({transition("@@", mk_ext_action(parse_partial_explicit_expr))}, x0);
     r = r.add({transition("!", mk_ext_action(parse_consume_args_expr))}, x0);
     r = r.add({transition("begin", mk_ext_action_core(parse_begin_end))}, x0);
     r = r.add({transition("begin+", mk_ext_action_core(parse_begin_end_plus))}, x0);

src/frontends/lean/pp.cpp

@@ -62,6 +62,7 @@ static format * g_from_fmt        = nullptr;
 static format * g_visible_fmt     = nullptr;
 static format * g_show_fmt        = nullptr;
 static format * g_explicit_fmt    = nullptr;
+static format * g_partial_explicit_fmt    = nullptr;
 static name   * g_tmp_prefix      = nullptr;
 
 class nat_numeral_pp {
@@ -126,6 +127,7 @@ void initialize_pp() {
     g_visible_fmt     = new format(highlight_keyword(format("[visible]")));
     g_show_fmt        = new format(highlight_keyword(format("show")));
     g_explicit_fmt    = new format(highlight_keyword(format("@")));
+    g_partial_explicit_fmt    = new format(highlight_keyword(format("@@")));
     g_tmp_prefix      = new name(name::mk_internal_unique_name());
     g_nat_numeral_pp  = new nat_numeral_pp();
 }

src/frontends/lean/token_table.cpp

@@ -98,7 +98,7 @@ void init_token_table(token_table & t) {
          {"esimp", 0}, {"fold", 0}, {"unfold", 0}, {"with_options", 0}, {"simp", 0},
          {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec}, {"abstract", g_max_prec},
-         {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
+         {"proof", g_max_prec}, {"qed", 0}, {"@@", g_max_prec}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
          {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},
          {"<d", g_decreasing_prec}, {"renaming", 0}, {"extends", 0}, {nullptr, 0}};

src/frontends/lean/token_table.h

@@ -18,7 +18,7 @@ Author: Leonardo de Moura
 namespace lean {
 // User-level maximum precedence
 unsigned get_max_prec();
-// Internal maximum precedence used for @ and ! operators
+// Internal maximum precedence used for @@, @ and ! operators
 unsigned get_Max_prec();
 unsigned get_arrow_prec();
 unsigned get_decreasing_prec();

src/frontends/lean/tokens.cpp

@@ -38,6 +38,7 @@ static name const * g_plus_tk = nullptr;
 static name const * g_star_tk = nullptr;
 static name const * g_turnstile_tk = nullptr;
 static name const * g_explicit_tk = nullptr;
+static name const * g_partial_explicit_tk = nullptr;
 static name const * g_max_tk = nullptr;
 static name const * g_imax_tk = nullptr;
 static name const * g_cup_tk = nullptr;
@@ -191,6 +192,7 @@ void initialize_tokens() {
     g_star_tk = new name{"*"};
     g_turnstile_tk = new name{"⊢"};
     g_explicit_tk = new name{"@"};
+    g_partial_explicit_tk = new name{"@@"};
     g_max_tk = new name{"max"};
     g_imax_tk = new name{"imax"};
     g_cup_tk = new name{"\u2294"};
@@ -345,6 +347,7 @@ void finalize_tokens() {
     delete g_star_tk;
     delete g_turnstile_tk;
     delete g_explicit_tk;
+    delete g_partial_explicit_tk;
     delete g_max_tk;
     delete g_imax_tk;
     delete g_cup_tk;
@@ -498,6 +501,7 @@ name const & get_plus_tk() { return *g_plus_tk; }
 name const & get_star_tk() { return *g_star_tk; }
 name const & get_turnstile_tk() { return *g_turnstile_tk; }
 name const & get_explicit_tk() { return *g_explicit_tk; }
+name const & get_partial_explicit_tk() { return *g_partial_explicit_tk; }
 name const & get_max_tk() { return *g_max_tk; }
 name const & get_imax_tk() { return *g_imax_tk; }
 name const & get_cup_tk() { return *g_cup_tk; }

src/frontends/lean/tokens.h

@@ -40,6 +40,7 @@ name const & get_plus_tk();
 name const & get_star_tk();
 name const & get_turnstile_tk();
 name const & get_explicit_tk();
+name const & get_partial_explicit_tk();
 name const & get_max_tk();
 name const & get_imax_tk();
 name const & get_cup_tk();

src/frontends/lean/tokens.txt

@@ -33,6 +33,7 @@ plus         +
 star         *
 turnstile    ⊢
 explicit     @
+partial_explicit @@
 max          max
 imax         imax
 cup          \u2294