Anh
On Tuesday, February 6, 2018 at 2:16:35 PM UTC+1, Stephan Merz wrote:
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 <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.