Zulip Chat Archive
Stream: lean4
Topic: (deleted)
Mac (Jul 06 2021 at 17:46):
(deleted -- confused t and t/tau)
Marcus Rossel (Dec 19 2023 at 17:21):
(deleted)
Alex J. Best (Dec 19 2023 at 17:25):
Do you need to add
initialize
Lean.registerTraceClass `xyz
in an earlier file and set_option trace.xyz true? or something like that
Last updated: Dec 20 2023 at 11:08 UTC