class HASHED_DICTIONARY_NODE [V_, K_ -> HASHABLE]

Features exported to HASHED_DICTIONARY

Auxilliary class to implement HASHED_DICTIONARY.

Direct parents

conformant parents

ANY_HASHED_DICTIONARY_NODE

Summary

creation features

exported features

Details

make (i: V_, k: K_, n: HASHED_DICTIONARY_NODE [V_, K_ -> HASHABLE])

ensure

  • item = i
  • key = k
  • next = n

item: V_
key: K_
next: HASHED_DICTIONARY_NODE [V_, K_ -> HASHABLE]

The next one when some clash occurs.

set_item (i: V_)

ensure

  • item = i

set_next (n: HASHED_DICTIONARY_NODE [V_, K_ -> HASHABLE])

ensure

  • next = n

make (i: V_, k: K_, n: HASHED_DICTIONARY_NODE [V_, K_ -> HASHABLE])

ensure

  • item = i
  • key = k
  • next = n