CODEWITHSUNDEEP
isabelle
Mathieu Paturel
Mathieu Paturel

Reputation: 4510

Meaning of isabelle clarsimp/fastforce's background turning light red

Image to fastforce with light red background

Image of clarsimp with light red background

This keeps happening in my proofs. As you can see, the proof goal window is blank. What does the light red background on fastforce mean? The same happends with clarsimp.

It seems to hang forever once that happens.

Upvotes: 0

Views: 40

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8298

Is there any additional output when you position the caret on the fastforce call? If yes, that will probably tell you what the problem is.

But my guess is that there is none, and in that case the problem is usually that the fastforce call diverges and eventually runs out of memory and crashes. That is usually the cause of lines in Isabelle being printed in red like this. This can have a number of reasons: excessive backtracking, a simplifier loop, etc.

Upvotes: 1

Related Questions