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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Wed, 29 Mar 2023 12:16:33 -0400

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.

**Follow-Ups**:

- Prev by Date:
**Re: [SOCIAL NETWORK] Re: [tlaplus] Resources for learning TLA+ proofs** - Next by Date:
**Re: [tlaplus] Resources for learning TLA+ proofs** - Previous by thread:
**Re: [tlaplus] Help understanding why this proof validates** - Next by thread:
**Re: [tlaplus] SANY error: Non-constant TAKE, WITNESS, or HAVE for temporal goal.** - Index(es):