deferred class interface HASHABLE
   --
   -- Ancestor class for all hashable objects.
   -- For example, the hash_code is needed for DICTIONARY and for SET.
   -- Thus, most standard objects are HASHABLE (STRING, DOUBLE, REAL, 
   -- INTEGER_8, INTEGER_16, INTEGER_32, INTEGER_64, POINTER, NUMBER,
   -- MUTABLE_BIG_INTEGER, etc.). 
   --

feature(s) from HASHABLE
   hash_code: INTEGER
      -- The hash-code value of Current.
      ensure
         good_hash_value: Result >= 0



end of deferred HASHABLE