Jan van Brügge (Dec 20 2022 at 15:31): Jan van Brügge (Dec 20 2022 at 15:31):In my current (apply script) proof I am using the subgoal command to focus on premises and parameters. But after solving the subgoal, when I use done I get an Option error in basics.ML. I think I had this once where I unfolded atomize_imp[symmetric] under the subgoal, but this time I am not doing that.
What could be the reason for this error? The proof is quite long and relies on other theorems so I can't really post it as reference
Jan van Brügge (Dec 20 2022 at 15:35):This is the error in jEdit (I have nested subgoal): image.png
Jan van Brügge (Dec 20 2022 at 16:03):Ok, my hunch was right, changing my proof to not use apply (unfold atomize_imp[symmetric] atomize_all[symmetric]) fixes this issue
Last updated: Dec 21 2024 at 16:20 UTC