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.
A dark purple background means that the proof didn't terminate yet.
It is possible that proof methods never terminate, e.g. when you have cyclic rewrite rules.
(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