[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] The function return the index of element in a queue
Thank you very much for your help.
On Tuesday, February 6, 2018 at 2:16:35 PM UTC+1, Stephan Merz wrote:
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 <thea...@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...@googlegroups.com.
> 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.