[tlaplus] Expanding PrintT to TRUE in proofs?

[JosEdu Solsona <josedusolsona@xxxxxxxxx>]

Hello,

According to Unsupported TLA+ features:

TLAPS has no built-in knowledge of (most of) the operators defined in the TLC standard module, and it cannot use their definitions either.

So, when trying to prove an obligation containing PrintT operator (which is defined to be TRUE in TLC module), TLAPS cant prove it unless the same PrintT was already in assumptions.

Should i comment out PrintT statements from specs when doing proofs?, or there is a better way?

Thanks

-- 
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/e1933e9f-0b9a-4658-a3c3-9fb74b8fdcb0%40googlegroups.com.