[cbc] Roding Proofs and the (R) button

Hi. I have been asked whether using the blue (R) button is a valid way to discharge proofs.

The short answer is no. The blue (R) button does *not* discharge any proof, as it does not try to prove anything. It stands for "Reviewed" and it is a way to tell Rodin "do not bother me with this proof; I am completely sure it's correct" or "I will do that later; I want to continue doing other things now".

So, blue bullets in the Proof Obligation panel on the right cannot be accepted as a discharged proof.

Best regards,