class TWO_WAY_LINKED_LIST_NODE [E_]

All features

To implement TWO_WAY_LINKED_LIST.

Direct parents

conformant parents

ANY_TWO_WAY_LINKED_LIST_NODE

Summary

creation features

exported features

Details

make (i: E_, p: TWO_WAY_LINKED_LIST_NODE [E_], n: TWO_WAY_LINKED_LIST_NODE [E_])

ensure

  • item = i
  • previous = p
  • next = n

item: E_
previous: TWO_WAY_LINKED_LIST_NODE [E_]
next: TWO_WAY_LINKED_LIST_NODE [E_]
make (i: E_, p: TWO_WAY_LINKED_LIST_NODE [E_], n: TWO_WAY_LINKED_LIST_NODE [E_])

ensure

  • item = i
  • previous = p
  • next = n

set_item (i: E_)

ensure

  • item = i

set_next (n: TWO_WAY_LINKED_LIST_NODE [E_])

ensure

  • next = n

set_all_with (v: E_)
set_previous (p: TWO_WAY_LINKED_LIST_NODE [E_])

ensure

  • previous = p