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

[tlaplus] Examples of specs with proofs that use subexpressions?

Been reading the TLA+2 language spec and had no idea that subexpressions existed and were so powerful. You can use the language itself to navigate around the parse tree of the TLA+ file you're working in! Are there any examples of TLAPS proofs which use this? Also, does TLC support it (although I assume it's quite inefficient)?


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/21cd1584-64a0-469e-bdb5-ddd8fd8d19dbn%40googlegroups.com.