Zulip Chat Archive

Stream: lean4

Topic: trace classes

Jakob von Raumer (Sep 16 2021 at 10:04):

What is needed to create a new trace class? builtin_initialize Lean.registerTraceClass <backtick>IIT.Totality doesn't enable me to do set_option trace.IIT.Totality true...

Leonardo de Moura (Sep 16 2021 at 13:54):

@Jakob von Raumer You have to use the initialize command. I added an example
https://github.com/leanprover/lean4/commit/a29e81b0b6eb305d47c6e8675187f254bf7d2e5c

Jakob von Raumer (Sep 16 2021 at 14:03):

Ah, right, thanks

Last updated: Dec 20 2023 at 11:08 UTC