what's the best way to testing

Stream: new members

[Xiyu Zhai]

I would like to know the accepted style of testing in Lean. If there could be a section on testing in function programming in lean, that would be great.

My trouble is I can't easily use #eval for testing. It forbids me from using things containing sorry. So is there something like panic or undefined? I don't want to use Monad every single time. But maybe I should.

[Arthur Paulino]

I don't think the Lean 4 ecosystem is mature enough such that the community has reached consensus on the best testing framework/style/lib yet

While we (Lurk Lab) were using Lean 4, we developed LSpec to test our implementations. See if it fits your needs: https://github.com/lurk-lab/LSpec