elabTerm with custom name resolution?

Stream: lean4

[Joachim Breitner]

Loogle/#find are probably much more ergonomic if one wouldn't have to specify all names qualified. Instead, it could, for unqualified names, see if that name exists qualified and use that, maybe with a warning, maybe only when its unambiguous.

For simple queries, I can do that easily.
But for queries that involve patterns, these run through Term.elabTerm – can I reasonably easily hook into the name resolution step of that function?