Spec/implementation differences between Theorem and Assume/Prove

[ahelwer]

According to the TLA+ language spec, this should be valid:

THEOREM thm == TRUE

However, SANY does not parse it. SANY does parse the following:

THEOREM thm == TRUE
<1> QED

So it seems it can be named as long as it is followed by a proof. However, it does not parse:

THEOREM thm == TRUE
OBVIOUS

edit: okay nevermind apparently it parses it now? I don't know.

[ahelwer]

SANY also does not like this:

THEOREM
  ASSUME asm :: 
    ASSUME 1
    PROVE 2
  PROVE 3
OBVIOUS

giving the error "Label not in definition or proof step". Although this might fall under the category of semantic error.

[ahelwer]

Chalking this one up to SANY weirdness