Zulip Chat Archive
Stream: lean4
Topic: lean4 analogue of `when_tracing`?
Scott Morrison (Mar 26 2023 at 09:14):
What are when_tracing and is_trace_enabled_for called now?
Scott Morrison (Mar 26 2023 at 22:19):
Answering my own question, sorry: isTracingEnabledFor.
Last updated: May 02 2025 at 03:31 UTC