[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Scope of the QED keyword


   What is the scope of the QED keyword? 

   In my understanding, at any point in a proof, the QED keyword represents the main goal of the level in which it is being used. That goal may be the main theorem of the proof or the goal of a step in a hierarchical proof.

   I am asking because I have not found this explicitly mentioned anywhere (maybe I have missed some part of the documentation).

Thank you

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8250cd95-844f-4bb8-8883-83ddc3fac8c7%40googlegroups.com.