Simon Cruanes

That's always been the case, even with the current simple `Buffer.t`. Allocating the exact size is not realistic imho. The better way is to reuse the encoder (with the recently...

Or, avoid bigstrings entirely, and return `(bytes,offset)` on demand :). That also has the benefit of not being horribly slow if people don't reuse the buffers, and avoids some dependencies.

If you do non blocking IOs, then yes. If you do blocking IOs you generally can directly use the byte buffer + offset :)

I found this very interesting document: https://perfetto.dev/docs/design-docs/protozero there's in particular mention of "scattered IO", which certainly must help with nested messages: > A key part of the ProtoZero design is...

Not sure if @benti can cook us a version of Zipperposition that is complete on this fragment :-)

So the problem seems to be the completion of positive equalities. From `f = g` the prover deduces `f x = g x`… and throws it away immediately after demodulating...

Yeah, I'm working on it, never mind :)

for some reason, right now, it doesn't (I do exactly this completion).

should be fixed in 1.6 by @benti and @petarvukmirovic and @gh-salt 's work.

use `open CCOrd.Infix` to avoid shadowing `compare` (safer)