Stream: Beginner Questions

Topic: Error Option when closing subgoal with done


view this post on Zulip 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

view this post on Zulip Jan van Brügge (Dec 20 2022 at 15:35):

This is the error in jEdit (I have nested subgoal): image.png

view this post on Zulip 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: Feb 27 2024 at 08:17 UTC