Zulip Chat Archive

Stream: lean4

Topic: Testing


view this post on Zulip Calvin Lee (Feb 21 2021 at 00:47):

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.

view this post on Zulip Bryan Gin-ge Chen (Feb 21 2021 at 00:48):

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

view this post on Zulip Calvin Lee (Feb 21 2021 at 01:35):

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


Last updated: May 18 2021 at 22:15 UTC