Idiomatic unit test

Stream: lean4

[Geoffrey Irving]

If I have a computational expression expr : Bool, and want to record a unit test that expr = True, I can do

lemma test : expr := by native_decide

Is this the most idiomatic way to express a unit test, or there is something better?

[Henrik Böving]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/How.20to.20unit.2Fdoc.20test.3F