Supplements to the Lean 4 Batteries.

All components are unstable but feel free to use whatever you need for your own project!


This is a miscellaneous repository of code that, for a variety of reasons, neither belonged in the standard library nor in development code. Ideally, everything in here will find its way elsewhere in due time.

That said: this is not a code dump! All the code in here is curated. Pull requests are very welcome but they will be carefully reviewed before merging.

  • The extra4 library is copyright © 2023-2024 François G. Dorais. The library is released under the Apache 2.0 license. See the file LICENSE for additional details.
  • Just ask if you need to use parts of this code under different licensing terms!