Implement a general Show typeclass in MetaCoq.Utils

[mattam82]

This allows to conveniently print anything for debugging purposes, or using the FFIs to print messages in the various extractions (the live and extracted ones, malfunction or certicoq)

[JasonGross]

If you want a version that does levels-based parenthesizing, Fiat Crypto has such a class: https://github.com/mit-plv/fiat-crypto/blob/master/src/Util/Strings/Show.v

[gmalecha]

ExtLib has a Show class and instances as well. Is there any interest in unifying things like this? Would people depend on another opam library to get Show with a bunch of instances for standard types, e.g. bool, nat, N, etc?

[JasonGross]

Does ExtLib do level-based printing, so that it can parenthesize as much as needed but not more?

In any case, it seems in #952 (comment) that we're receptive to depending on extlib

[gmalecha]

ExtLib does not do level based printing that I am aware of. The underlying setup is parameterized by a Monoid with an injection from Ascii I think. You could add a wrapper for a level though to get this extra functionality.

My main motivation is to avoid repeated work, if you benefit from this, other might as well and that would make for reducing overall maintenance.