feat(frontends/lean): basic support for partial explicit

src/frontends/lean/builtin_exprs.cpp

@@ -691,7 +691,15 @@ 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());
+    expr e = p.parse_expr(get_Max_prec());
+    if (is_choice(e)) {
+        buffer<expr> new_choices;
+        for (unsigned i = 0; i < get_num_choices(e); i++)
+            new_choices.push_back(p.save_pos(mk_partial_explicit(get_choice(e, i)), pos));
+        return p.save_pos(mk_choice(new_choices.size(), new_choices.data()), pos);
+    } else {
+        return p.save_pos(mk_partial_explicit(e), pos);
+    }    
 }
 
 static expr parse_consume_args_expr(parser & p, unsigned, expr const *, pos_info const & pos) {

src/frontends/lean/pp.cpp

@@ -153,6 +153,7 @@ void finalize_pp() {
     delete g_from_fmt;
     delete g_visible_fmt;
     delete g_show_fmt;
+    delete g_partial_explicit_fmt;    
     delete g_explicit_fmt;
     delete g_tmp_prefix;
 }

src/library/explicit.cpp

@@ -46,6 +46,7 @@ void initialize_explicit() {
     g_consume_args_name = new name("!");
 
     register_annotation(*g_explicit_name);
+    register_annotation(*g_partial_explicit_name);    
     register_annotation(*g_as_atomic_name);
     register_annotation(*g_as_is_name);
     register_annotation(*g_consume_args_name);