Lean Collections Library

General-purpose collections implemented in pure Lean 4.

LeanColls attempts to make programming and proving with collections a fun and straightforward experience. To that end, the library contains:

1. Comprehensive interfaces for common collection operations.
2. Lawfulness specifications for those interfaces.
3. Performant & proven-correct implementations.
4. Utilities for writing clean, efficient, and provably correct code with collections.

which is quite a lot!

More thorough documentation is WIP. Contributions are welcome and appreciated; see the GitHub repository.