Zulip Chat Archive

Stream: lean4

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


Siddharth Bhat (Jul 05 2022 at 22:47):

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 (Jul 05 2022 at 22:51):

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 (Jul 06 2022 at 06:36):

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


Last updated: Dec 20 2023 at 11:08 UTC