checking for `sorryAx` in elaborated terms

Stream: lean4

[Siddhartha Gadgil]

What is the best way to check whether a term obtained by elaboration has sorryAx in it? I am using Term.synthesizeSyntheticMVarsNoPostponing
Incidentally, this seems like a change in behaviour - in the past if I am correct exceptions were thrown in many cases where now sorry's are filled in.

[Alexander Bentkamp]

Maybe using Lean.Elab.Command.CollectAxioms.collect?

[Siddhartha Gadgil]

That seems to be for names. I have an expression generated by elabTerm.

[Alexander Bentkamp]

Oh, right. Of course one way would be to iterate through all subterms and check if they are sorryAx, but I guess your question is if the insertion of the sorry can be detected directly?

[Alexander Bentkamp]

Oh, there is also Expr.hasSyntheticSorry.