Topic: tactic debug
Patrick Massot (May 31 2018 at 20:44):
Is there anything like a Lean debugger which would allow me to execute tactics line by line and inspect the values of variables? Or should I add trace commands after every lines in Simon's tactics to hope to understand how they work?
Gabriel Ebner (Jun 01 2018 at 06:48):
There is a debugger, but I don't think anybody here uses it (or even knows how to use it). You need to run it from the command-line. Example: https://github.com/leanprover/presentations/blob/master/20170116_POPL/debug/has_to_string_break.lean I'd stick to trace messages.
Patrick Massot (Jun 01 2018 at 06:54):
Last updated: May 13 2021 at 05:21 UTC