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

[Stephan Merz <stepha...@xxxxxxxxx>]

Hello,

probably the easiest way is to use a CHOOSE expression:

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

Regards,
Stephan


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