do we have `fillImplicitArgumentsWithFreshMVars`?

Stream: lean4

[Scott Morrison]

I found myself wanting:

partial def fillImplicitArgumentsWithFreshMVars (e : Expr) : MetaM Expr := do
  match ← inferType e with
  | Expr.forallE _ _ _ .implicit => do
    fillImplicitArgumentsWithFreshMVars (mkApp e (← mkFreshExprMVar none))
  | _                    => pure e

but I feel like it must exist somewhere already, or have a better implementation.

Any suggestions?

[Scott Morrison]

(See https://github.com/leanprover-community/mathlib4/pull/1476/files#diff-d272d0233c9cb593439825761f1a8bcb5858ebc28d1bba77f6199ffbf9046e30R28 for the application.)

[Jannis Limperg]

I'm not aware of an existing function that does this, but it seems useful. I would implement it with forallTelescope (or one of its variants, if you want to discover implicit arguments up to computation).