# [tlaplus] Eliminate random element from seq

Hi, i want to write a function that given a sequence will return a sequence as the one passed but without one element at random, this is my solution but it is wrong, someone can tell me why? And what would be a correct solution? Thanks

EXTENDS Integers, Sequences

Remove(i, seq) ==

[j \in 1..(Len(seq)-1) |-> IF j < i THEN seq[j]

ELSE seq[j+1]]

Random(S) ==  CHOOSE x \in S : TRUE

Err(seq) ==

Remove(Random({1..Len(seq)}), seq)

--
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+unsubscribe@xxxxxxxxxxxxxxxx.