Is code displayed at the infoview guaranteed to be well-typ?

Stream: lean4

[Siddharth Bhat]

I had a situation where copy-pasting an expression from the InfoView produced an expression that failed to #check (ie, the expression type errors). On the other hand, using set_option pp.all true (as suggested by @Sébastien Michelland ) produced a gargantuan expression that did pass the #check (ie, Lean inferred the correct type for this expression).

In general, are the expressions that are displayed in the InfoView guaranteed to be well-typed in their context? Said differently, should I try to find an MWE for the case I ran into?

[Leonardo de Moura]

No, there is no guarantee that any term there can be re-elaborated. The focus is on readability.
The option set_option pp.analyze true is between the default and pp.all, it often generates terms that can be re-elaborated, but it is not perfect.

[Eric Wieser]

Is the output with pp.all intended to always re-elaborate?