diff --git a/Remove.tla b/Remove.tla new file mode 100644 index 0000000..8f27ec1 --- /dev/null +++ b/Remove.tla @@ -0,0 +1,12 @@ +------------------------------- MODULE Remove ------------------------------- + +EXTENDS Integers, Sequences + +Remove(i, seq) == + [j \in 1..(Len(seq)-1) |-> IF j < i THEN seq[j] + ELSE seq[j+1]] + +============================================================================= +\* Modification History +\* Last modified Mon Jan 14 16:12:46 CET 2019 by veitheller +\* Created Mon Jan 14 16:12:39 CET 2019 by veitheller