Comment by staunton

Most (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.