leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover
Apache License 2.0
253 stars 105 forks source link

chore: turn batteries tests into a library #1024

Closed edegeltje closed 3 weeks ago

edegeltje commented 3 weeks ago

see also this PR to mathlib, this discussion of that PR on zulip, and the discussion leading to this PR

tldr; this allows you to write tests for importing behaviour without "contaminating" the library proper with test data.

leanprover-community-bot commented 3 weeks ago

Mathlib CI status (docs):