The function return the index of element in a queue

[the anh pham]

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?

[Stephan Merz]

Hello,

probably the easiest way is to use a CHOOSE expression:

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

Regards,
Stephan

> --
> 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...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[the anh pham]

Dear Stephan,

Thank you very much for your help. 

Best regards,

Anh