On 08.08.20 17:52, Mario Carneiro wrote:> .... > Also, is there any way for me to do "printf debugging" in isabelle/ML? > The focus on pure functional programming makes debugging especially > difficult, but I'm sure I'm just missing the idioms for doing so > (understandably, I can't find any examples of debugging in the source).
The ML-cookbook has a section (2.2) about debugging that might help you: https://nms.kcl.ac.uk/christian.urban/Cookbook/ Some combinators (like "tap") might also speed up your development (see section 2.3). > Currently I'm in the first stage, which involves modifying primarily > thm.ML and proofterm.ML to support "proof traces" instead of "proof > terms". Do you mind giving more details about what you mean by "proof traces" in this context? Best wishes, Kevin _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
