[tlaplus] Scope of the QED keyword

[Saswata Paul <paulsaswata1@xxxxxxxxx>]

Hi,

   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.