[an error occurred while processing this directive]

Table of Contents Previous Chapter

5.23 Class DOUBLE_REF

indexing
class interface
feature -- Access
-- Double value
-- Hash code value
-- (From HASHABLE.)
good_hash_value: Result >= 0
feature -- Element change
-- Make d the associated double value.
item_set: item = d
end

Table of Contents Next Chapter