To implement LINKED_LIST. |
make (i: E_, n: LINKED_LIST_NODE [E_]) |
ensure
|
item: E_ |
next: LINKED_LIST_NODE [E_] |
make (i: E_, n: LINKED_LIST_NODE [E_]) |
ensure
|
set_item (i: E_) |
ensure
|
set_next (n: LINKED_LIST_NODE [E_]) |
ensure
|
set_all_with (v: E_) |