Gergely Buday (Jan 20 2021 at 10:53): Gergely Buday (Jan 20 2021 at 10:53):According to
https://stackoverflow.com/questions/22635300/what-do-colour-codes-mean-in-isabelle-jedit
purple is "running process on the command"
If that command is a by (simp add:lemma), then it went to infinite loop? Other than that, it led to No Subgoals! Is this a valid proof or not?
Manuel Eberl (Jan 20 2021 at 11:00):If it is just purple indefinitely, it means that it has not terminated yet. As I explained in the other thread, that means that the proof is not yet completed. The ‘No subgoals!’ you see is provisional in the sense that it assumes that the proof is valid (which it isn't if the simp never terminates).
Mathias Fleury (Jan 20 2021 at 11:08):(@Manuel Eberl : I got confused when reading your sentence, but I guess "yeat complicated" -> yet completed)
Manuel Eberl (Jan 20 2021 at 11:09):Uh, probably.
Manuel Eberl (Jan 20 2021 at 11:10):Not sure what happened there. Probably general brain fault. :smile:
Manuel Eberl (Jan 20 2021 at 11:10):Temporary aphasia.
Gergely Buday (Jan 20 2021 at 11:11):Thanks. At last I have found the necessary lemmas so now it works without problem.
Gergely Buday (Jan 20 2021 at 11:15):Also, it used lots of processor and memory, that's why I thought of an infinite loop.
Last updated: Dec 21 2024 at 16:20 UTC