Simplify Show about coq-ext-lib HOT 7 OPEN

I am generally in favor of small libraries, so I would be in favor of moving Show somewhere else.

I don't think that S-expressions solve everything, so I think there is some benefit to more customizable pretty printing library. Perhaps there is some good way to share some of the formatting logic within ceres? I'm thinking of "boxes" and the like.

from coq-ext-lib.

Another option is to deprecate and remove Show altogether. Even if we fixed it, it seems a good candidate to put into its own library.

I recently created coq-ceres as an alternative, using S-expressions instead of strings as a common format that can easily be pretty-printed and parsed.

A proper pretty-printing library also seems like a good idea.

from coq-ext-lib.

@Lysxia Do you think there is some pieces of ceres that could be reused for this?

from coq-ext-lib.

from coq-ext-lib.

Does ceres not generate a string?

from coq-ext-lib.

I'm not sure what you're thinking of. There is a function that converts S-expressions (trees) to strings, but there's not much to be reused from it.

from coq-ext-lib.

I see.

from coq-ext-lib.