automated testing

Stream: general

[Vadim Fomin]

What's the Lean way to run automated tests in Lean projects? Is there a Lean analogue to Python's pytest or unittest?

[Asei Inoue]

you can register test_driver function

[Asei Inoue]

then run lake test in terminal.

[Asei Inoue]

I don’t know popular test library of Lean.
But there is a library called plausible for property test.

[Asei Inoue]

you can use just #guard or example command for unit test.

[Daniil Kisel]

See also: LSpec, specs, nest.