# Re: [tlaplus] How to define an invariant that describes a sorted sequence

Thanks! That worked.

Pramod

On Sat, Jan 26, 2019 at 10:52 PM Stephan Merz <stepha...@xxxxxxxxx> wrote:
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

On 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 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.