Xia Li-yao

#315 adds mention of where the output location is. It would still be nice to make the output more visible in vscoq in the first place.

I'm not sure whether the constructor is intentionally hidden, but since it's an instance of `Integral` you can easily convert to and from it with `fromIntegral`. What you describe is...

#1 suggests that this kind of thing can happen, but I'm not sure why.

I'm surprised GHC can still optimize these sufficiently for `inspection-testing` to see that they are the same. How could we make `ghc-proofs` work with recursive definitions? GHC doesn't expose unfoldings...

Here's an example from my `profunctor-monad`: ``` replicateP_ :: (Profunctor p, Applicative (p [x])) => Int -> p x a -> p [x] [a] replicateP_ 0 _ = pure []...

We can even keep it safe by just redefining `KeyMap` using `Map Text`

One way to search the literature is to find any related work (in this case, Okasaki's thesis), and then look up papers citing and cited by it in Google Scholar,...

I can't guarantee you'll find something worthwhile, but two papers that caught my eye are - http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=BA916D23E3FFE7C508883C0CBC5CCEBC?doi=10.1.1.13.3451&rep=rep1&type=pdf - http://www.cphstl.dk/Paper/Strictly-regular-number-system/final.pdf

I think the idea is not to get rid of CPP altogether, but to rewrite the CPP so that the chosen formatter can handle it, or make some feature requests...

I've managed to load custom syntax definitions like this https://bitbucket.org/lyxia/blog.poisson.chat/src/70d2c905b6a3d663cc0494137e0921d3bd0b0e40/site.hs?at=master&fileviewer=file-view-default#site.hs-40:45 Although, I would also like to know whether there is a more hakyllesque solution (hakyll doesn't see me loading the...