It’s probably just because a zstd implementation in Lean would be more difficult. The whole project depends on being able to have a correctness proof for the implementation, and implementing that for the DEFLATE algorithm is simpler.
replyreply
The pure Lean implementation of zstd in that project is only decompression, not compression. It kind of proves my point.
reply