Lukas Stevens (Nov 11 2020 at 16:55): Lukas Stevens (Nov 11 2020 at 16:55):I declared an attribute that controls whether a tactic of mine prints debug information. What is the correct way to really print the information? Currently, I am doing something like this
...
val _ = if Config.get ctxt order_debug_cfg then (@{print} x; ()) else ()
...
If you already have strings, then there is a function calledtracing ( string -> unit)
Lukas Stevens (Nov 11 2020 at 17:02):Does this trace with the same mechanism as @{print}?
Mathias Fleury (Nov 11 2020 at 17:04):it is printed in the same panel and it is used in ~~/src/HOL/Tools for that purpose
Mathias Fleury (Nov 11 2020 at 17:06):on the other hand, argo in the same folder uses a different mechanism…
Last updated: Oct 31 2025 at 20:23 UTC