chore(frontends/lean/builtin_cmds): support 'sorry' at #elab command

src/frontends/lean/builtin_cmds.cpp

@@ -669,6 +669,8 @@ static expr replace_with_simple_metavars(metavar_context & mctx, expr const & e)
 
 static environment elab_cmd(parser & p) {
     expr e = p.parse_expr();
+    if (p.used_sorry())
+        p.declare_sorry();
     metavar_context mctx;
     expr new_e; level_param_names ls;
     std::tie(new_e, ls) = p.elaborate(mctx, e);

tests/lean/run/elab3.lean

@@ -0,0 +1,3 @@
+set_option pp.binder_types true
+
+#elab (sorry : ∀ a, a > 0)