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.
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.