Xia Li-yao

I tried MetaCoq a bit; it's promising but still a bit early for serious usage. It seems we need a generic-lib on top of it. Here's some discussion about my...

So after thinking about the plan a bit more, maybe the split outlined above is a bit too ambitious. I think the most important thing is to keep the plugin...

I would accept the implementation mentioned in an earlier comment: ``` isSubsequenceOf needles haystack = List.isSubsequenceOf (T.unpack needles) (T.unpack haystack) ``` If you want to stick to the current implementation,...

Is it better to extend `Arbitrary` instead of creating a different class for this?

In other words, I think you can just drop the comment about optimality.

I may be missing some context. IIUC it seems the difference is not forcing the vectors when you force the spine. - How is `length` logarithmic time (and why was...

I feel like the access patterns this would benefit are too peculiar to be worth it. It's easier to say that random access, and operations like `length` that must have...

The upper bound was to work around a bug (discussed [here](https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/.5BERROR.5D.20The.20comp**.20of.20coq-core.2Edev.20failed.20at.20.22dune.20subst.22.2E)) that manifests itself on opam CI with dune 3.14. So if this PR doesn't pass CI, a more local...

Nice one!

Fixed because QuickChick is now being installed via dune.