18 ms·
If you're interested in this stuff at all, check out some code. Example: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/Mathlib/Algebra/GroupWithZe
by lincolnq 2y ago
If you're interested in this stuff at all, check out some code.
Example: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...
Also check out the blueprint, which describes the overall structure of the code:
https://imperialcollegelondon.github.io/FLT/blueprint/ https://imperialcollegelondon.github.io/FLT/blueprint/
I'm very much an outside observer, but it is super interesting to see what Lean code looks like and how people contribute to it. Great thing is that there's no need for unittests (or, in some sense, the final proof statement is the unittest) :P
- staunton 2y agoMost (larger) Lean projects still have "unit tests". Those might be, e.g., trivial examples and counter examples to some definition, to make sure it isn't vacuous.
- schoen 2y agoThat's such a nice way to think about unit tests! (In this context and others.)
- pierrefermat1 2y agoI think the better mapping of unit tests would actually be proofs of lemmas ?
- staunton 2y agoI don't see why you would think that. In such a project theorems and proofs are "the main point of the software". The unit tests make sure certain things don't go wrong by noticing when developers, e.g., mess up while refacing something. Also, people actually put the things I was talking about in a folder called "test"...