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: Dec 20 2023 at 11:08 UTC