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,StephanOn 26 Jan 2019, at 18:05, Pramod Biligiri <pramodb...@xxxxxxxxx> wrote: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 Ordereddefine
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.
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.