7 lines
205 B
Text
7 lines
205 B
Text
---- MODULE l09_remove ----
|
|
EXTENDS Integers, Sequences, TLC
|
|
|
|
Remove(i, seq) == [j \in 1..(Len(seq) - 1) |-> IF j < i THEN seq[j] ELSE seq[j+1] ]
|
|
|
|
ASSUME PrintT(<<"Eval", Remove(3, <<1, 2, 3, 4>>)>>)
|
|
====
|