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.
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.
https://github.com/kim-em/lean-zstd
The pure Lean implementation of zstd in that project is only decompression, not compression. It kind of proves my point.