class LINKED_LIST_NODE [E_]

All features

To implement LINKED_LIST.

Direct parents

conformant parents

ANY_LINKED_LIST_NODE

Summary

creation features

exported features

Details

make (i: E_, n: LINKED_LIST_NODE [E_])

ensure

  • item = i
  • next = n

item: E_
next: LINKED_LIST_NODE [E_]
make (i: E_, n: LINKED_LIST_NODE [E_])

ensure

  • item = i
  • next = n

set_item (i: E_)

ensure

  • item = i

set_next (n: LINKED_LIST_NODE [E_])

ensure

  • next = n

set_all_with (v: E_)