[tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

I ran into this error when writing theorems like:

THEOREM Spec => []Invariant

PROOF

  <1> HAVE Spec

  <1> ...

  <1> QED

If I replace it with this then SANY stops complaining:

THEOREM Spec => []Invariant

PROOF

  <1> SUFFICES ASSUME Spec PROVE []Invariant OBVIOUS

  <1> ...

  <1> QED

Why is the second one okay but the first one is not? I thought the first one was just shorthand for the second.

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/CABj%3DxUW4ayrmf%2BsVxViXOmpj0QSGb%3DvRCpUwmqn%3D1QVygirEOQ%40mail.gmail.com.