[tlaplus] What resources exist documenting the finer points of TLA+ language interpretation?

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

For example, how would I answer questions like:

• When defining macros, do we allow a space like macroname (arg1, arg2) == ...
  
• How exactly does evaluation of conjuncts/disjuncts with different indentation work
• etc.

Please note I am not asking these specific questions (because there are many more than that and I don't want to bore you); I'm asking what resources exist that would enable me to know the answer to such questions. So far I've found:

• The Operators of TLA+ [Lamport, 1997]
• Specifying Systems
• Trying & seeing what SANY accepts

Is there... a TLA+ spec of TLA+? :)

Andrew

-- 
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/b0b35999-e56d-4c3c-a040-df66e280e4can%40googlegroups.com.