| The syntax for quantifiers bounds is "variable \in set", the _expression_ "i < j" doesn't fit that pattern. You want to write
\A i \in 1..Len(myList), j \in 1..Len(myList) : i < j => myList[i] < myList[j]
Regards, Stephan
Hi, I'm trying to define an invariant that specfies a sequence should be (strictly) ordered, and am not getting the correct syntax. My sequence is called myList and the invariant is called Ordered
define
Ordered == \A i \in 1..Len(myList), j \in 1..Len(myList), i < j: myList[i] < myList[j]
end define;
Thanks, Pramod
--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|