Xia Li-yao

We could also use notations that eta expand all combinators, that would also be more efficient in general.

I added a new combinator so it's at least possible to work around this manually. I'm still not sure what the best way to fix the notations is. Full laziness...

It may be alright. I can't think of a good example where we pay for more than a constant factor. I applied your solution in `fc3bc8e`. It doesn't seem possible...

> printTestCase (show x ++ newline) (pf x)). Oh god. Good catch!

Thanks for reporting this issue. We indeed need some work to support native ints. 1. We must be able to tell QuickChick where to find the `Uint63` module (I'm not...

It would also be nice to make `Show` produce S-expressions (which might also be parsed as Gallina expressions) rather than strings. It decouples serialization from layout (pretty-printing) and makes parsing...

I created https://github.com/Lysxia/coq-ceres to replace Show.

I really think we should move away from flat strings, they make our life harder than necessary. They are annoying to write (deriving doesn't cover all cases, yet), and tightly...

I would stick with extlib for the monad class for now, and wait to split when the API can be substantially improved at the same time. There is definitely a...

The point of S-expressions is that a generic `show` should produce tree-shaped data rather than raw strings. So coq-ceres is very much intended to make coq-show unnecessary.