chore(library/delayed_abstraction): clarify delayed_abstraction API

src/frontends/lean/elaborator.cpp

@@ -3619,7 +3619,7 @@ static expr replace_with_simple_metavars(metavar_context mctx, name_map<expr> &
                         buffer<name> ns; buffer<expr> es;
                         get_delayed_abstraction_info(e, ns, es);
                         expr mvar_type = mctx.instantiate_mvars(decl->get_type());
-                        mvar_type      = push_delayed_abstraction(mvar_type, ns, es);
+                        mvar_type      = append_delayed_abstraction(mvar_type, ns, es);
                         expr new_type  = replace_with_simple_metavars(mctx, cache, mvar_type);
                         expr new_mvar  = mk_metavar(mlocal_name(mvar), new_type);
                         return some_expr(new_mvar);

src/library/delayed_abstraction.cpp

@@ -210,7 +210,7 @@ expr push_delayed_abstraction(expr const & e) {
     }
 }
 
-expr push_delayed_abstraction(expr const & e, buffer<name> const & ns, buffer<expr> const & vs) {
+expr append_delayed_abstraction(expr const & e, buffer<name> const & ns, buffer<expr> const & vs) {
     return push_delayed_abstraction_fn(ns, vs)(e);
 }
 

src/library/delayed_abstraction.h

@@ -13,8 +13,15 @@ expr mk_delayed_abstraction(expr const & e, name const & n);
 bool is_delayed_abstraction(expr const & e);
 expr const & get_delayed_abstraction_expr(expr const & e);
 void get_delayed_abstraction_info(expr const & e, buffer<name> & ns, buffer<expr> & es);
+/* Given a delayed abstraction `[delayed t, h_1 := e_1, ..., h_n := e_n]`, push
+   the delayed substitutions `h_i := e_i` to the metavariables occurring in `t`.
+
+   Remark: if `t` is a metavariable, then we just return `e`. */
 expr push_delayed_abstraction(expr const & e);
-expr push_delayed_abstraction(expr const & e, buffer<name> const & ns, buffer<expr> const & es);
+/* Append the new delayed substitutions `ns[i] := es[i]` to the metavariables occurring in `e`.
+
+   \pre ns.size() == es.size() */
+expr append_delayed_abstraction(expr const & e, buffer<name> const & ns, buffer<expr> const & es);
 
 /* Create e{ls[0] := ls[0], ..., ls[n-1] := ls[n-1]}
    \pre is_metavar(e)

src/library/metavar_util.h

@@ -24,6 +24,8 @@ bool is_assigned(expr const & e) const;
 optional<expr> get_assignment(expr const & e) const;
 void assign(expr const & m, expr const & v);
 
+push_delayed_abstraction
+
 bool in_tmp_mode() const;
 */
 
@@ -205,7 +207,7 @@ public:
         expr r = visit(e);
         if (m_found_delayed_abstraction) {
             buffer<name> ns; buffer<expr> es;
-            r = push_delayed_abstraction(r, ns, es);
+            r = append_delayed_abstraction(r, ns, es);
         }
         return r;
     }

src/library/type_context.cpp

@@ -1139,7 +1139,7 @@ expr type_context::infer_macro(expr const & e) {
         get_delayed_abstraction_info(e, ns, es);
         auto d = m_mctx.find_metavar_decl(mvar);
         if (!d) throw_unknown_metavar(mvar);
-        return push_delayed_abstraction(d->get_type(), ns, es);
+        return append_delayed_abstraction(d->get_type(), ns, es);
     }
     auto def = macro_def(e);
     bool infer_only = true;