I even do _ : (f x y) == expected; _ = refl makes tests shorter. I also put my tests in the same file that define them by adding a private module mod

I even do _ : (f x y) == expected; _ = refl makes tests shorter. I also put my tests in the same file that define them by adding a private module module X record X : ... private module test where _ : (f x y) == expected; _ = refl This way it's not possible to export record X without its tests passing.