trace without ToMessageData (etc.)

Stream: lean4

[Thomas Murrills]

Is there a way to just print "the expression" for debugging (in trace[...] "{a}", dbg_trace a, or via some other method)? Often I get a message like "failed to synthesize instance of ToMessageData ..." (or ToString ...).

Often I just want to see a simple structure instance or an inductive type constructor application, so I feel there must be a (uniform) way.

[Gabriel Ebner]

Is there a way to just print "the expression"

The "expression" doesn't exist at runtime. You only have the memory representation (which is like ctor_0(0, ctor_2(1, "abc"))) and we don't have a generic way to print in-memory objects.

[Thomas Murrills]

Hmm…do you think it would at all be possible (or even a good idea) to create e.g. a low-priority default instance of ToMessageData/ToString for all structure instances and inductive types, which just prints them “as you’d expect” (and ofc relied on similar instances for its field values/arguments)? It would make debugging a lot more convenient.

[Thomas Murrills]

Or is there a better way to debug when in this situation?

[Gabriel Ebner]

It would indeed be nice to have a deriving ToMessageData, Repr, ToString.