Jan van Brügge (Mar 26 2024 at 16:35): Jan van Brügge (Mar 26 2024 at 16:35):While developing bigger theorems with ML, it is quite useful to skip proofs that I am already done with, so they are not reloaded every time I reload the ML file.
I can of course do this with declare [[quick_and_dirty]] such that all my calls to Goal.prove_sorry skip the prove. However, inserting val lthy = Config.put quick_and_dirty false lthy before the proof I am working on still skips it.
OTOH, using Config.put before calling my other code somehow does not propagate to other ML files I call, even though I pass the same lthy around
So how can I skip the first part of my ML proofs, while still doing the rest?
Jan van Brügge (Mar 26 2024 at 16:46):My bad, apparently I modified the wrong lthy, declare [[quick_and_dirty]] together with Config.put works
Last updated: Dec 21 2024 at 16:20 UTC