Elaborating unknown identifiers

Stream: lean4

[Chris Bailey]

Is there a way to elaborate a term while doing something principled with unknown identifiers, like turning them into metavariables or getting back information about their Syntax elements?

The current behavior is to throw the error message, then replace the element with a synthetic sorry; if there's an easy way to map each sorry to the syntax element it came from I would be happy with that.