Stream: Beginner Questions

Topic: Black proof instead of red


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

view this post on Zulip Lukas Stevens (Jun 30 2021 at 08:35):

A dark purple background means that the proof didn't terminate yet.

view this post on Zulip Lukas Stevens (Jun 30 2021 at 08:35):

It is possible that proof methods never terminate, e.g. when you have cyclic rewrite rules.

view this post on Zulip 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: Sep 25 2021 at 08:21 UTC