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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 28 Apr 2020 09:02:33 +0200*References*: <e1933e9f-0b9a-4658-a3c3-9fb74b8fdcb0@googlegroups.com>

Yes, you should comment out PrintT for proofs. Since PrintT is evaluated only for its side effect, expanding the definition would probably be harmless. But this is not the case for other operators defined in the TLC module. For example, TLC evaluates x \in Any to TRUE, for any x, but this could not be proved based on the definition of Any and even worse, adding the axiom "\A x : x \in Any" would make the logic of TLA+ inconsistent. (It is harmless for finite domains that TLC is based on.) But you are raising an interesting question. We should probably reconsider which operators could and should be supported in proofs. Regards, Stephan
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/C6794C96-C148-46CB-AC60-43AD200E93B4%40gmail.com. |

**References**:**[tlaplus] Expanding PrintT to TRUE in proofs?***From:*JosEdu Solsona

- Prev by Date:
**[tlaplus] Expanding PrintT to TRUE in proofs?** - Next by Date:
**[tlaplus] Model Checking Specs having Nat** - Previous by thread:
**[tlaplus] Expanding PrintT to TRUE in proofs?** - Next by thread:
**[tlaplus] Model Checking Specs having Nat** - Index(es):