zero overhead debug tracing in pure code?

Stream: lean4

[Siddharth Bhat]

What's the lean equivalent of

#ifdef VERBOSE
printf("debug logging here");
#endif

In particular, I am looking for a way to insert debug logging into my pure code, such that when the project is built in release mode, the debug print has zero overhead. It would be even cooler if in debug mode, the printing can be toggled by a trace class.

[Mario Carneiro]

Does lean even have a debug mode?

[Mario Carneiro]

You should be able to hack something together using a term elaborator that is a no-op if some set_option is set