class HASHED_SET_NODE [E_ -> HASHABLE]

All features

Auxilliary class to implement HASHED_SET.

Direct parents

conformant parents

ANY_HASHED_SET_NODE

Summary

creation features

exported features

Details

make (i: E_, n: HASHED_SET_NODE [E_ -> HASHABLE])

ensure

  • item = i
  • next = n

item: E_
next: HASHED_SET_NODE [E_ -> HASHABLE]

The next one when some clash occurs.

set_next (n: HASHED_SET_NODE [E_ -> HASHABLE])

ensure

  • next = n

make (i: E_, n: HASHED_SET_NODE [E_ -> HASHABLE])

ensure

  • item = i
  • next = n