Testing

Stream: lean4

[Calvin Lee]

Is there any way to write tests for lean4 code?
I have some complex behavior that I would like to test (i.e. it is difficult to prove it in general). I could #eval it and check if it is true, but that isn't very satisfactory.

[Bryan Gin-ge Chen]

There was a recent thread on unit testing in Lean 4 here.

[Calvin Lee]

Oh this is helpful! thank you.
External dependencies in lean 4 still seem a bit rough around the edges though.