TL;DR: lean-containers is a type-safe, mathematically rigorous container library for Lean 4. It provides container signatures, polynomial functors, W-types (initial algebras), M-types (final coalgebras), and a battery of production-grade operations with lawful functor instances, proofs, and a minimal runtime footprint. Built for people who want correct-by-construction data structures in Lean—both for research and real systems.Repo: https://github.com/fraware/lean-containers
Status: Production Ready | Version: 1.0.0 | Lean: 4.8.0+