Zulip Chat Archive
Stream: lean4
Topic: qsort verification
Robin Arnez (Jul 08 2025 at 19:00):
tests/lean/run/grind_qsort.lean mentions:
-- TODO: when `grind` is ready for production use, move this file to `src/Init/Data/Array/QSort/Lemmas.lean`.
grind is now available to be used in production, so should this happen by now?
Asei Inoue (Jul 09 2025 at 06:30):
nice
Last updated: Dec 20 2025 at 21:32 UTC