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

Re: [tlaplus] The function return the index of element in a queue


probably the easiest way is to use a CHOOSE expression:

getIndex(e,seq) == CHOOSE n \in DOMAIN seq : seq[n] = e


> On 6 Feb 2018, at 14:10, the anh pham <thean...@xxxxxxxxx> wrote:
> Hello every one,
> I am a beginner of TLA. I have an issue and I hope you can help me.
> I want to have a function: getIndex(e, seq) in which e is a value in seq, seq is a sequence. This function must return the index of e in the seq (e is unique in seq)
> Coul you help me, please? 
> -- 
> 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.