Nicolò Cavalleri (Jun 29 2021 at 23:05): Nicolò Cavalleri (Jun 29 2021 at 23:05):What does it mean when a proof gets highlighted in red (and black on the side)? That is not being processed? In my file proofs of the kind by (transfer, auto)+ remained coloured in black and it is hard for me to understand what's wrong as in the output I cannot see any error message.
Lukas Stevens (Jun 30 2021 at 08:35):A dark purple background means that the proof didn't terminate yet.
Lukas Stevens (Jun 30 2021 at 08:35):It is possible that proof methods never terminate, e.g. when you have cyclic rewrite rules.
Manuel Eberl (Jun 30 2021 at 08:43):(transfer, auto)+ seems fishy. If the auto is unable to solve all the goals, you will just call transfer on the first remaining subgoal again. This will clearly never terminate if the auto is unable to solve the goal.
Not sure what your situation is precisely, but something like by (transfer; auto; fail)+ might be more robust.
Last updated: Dec 21 2024 at 16:20 UTC