indexing
description: ""
author: "David Solal"
date: "$ Date: "
revision: "$ Revision: "
class interface
INTEGER_KEY
create
make (type: like item)
BASIC_KEY
feature
make (type: like item)
BASIC_KEY
feature
item: INTEGER_REF
feature
hash_code: INTEGER
BASIC_KEY
ensure HASHABLE
good_hash_value: Result >= 0
Is_basic: BOOLEAN is True
BASIC_KEY
feature
is_hashable: BOOLEAN
HASHABLE
ensure HASHABLE
ok_if_not_default: Result implies (Current /= default)
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- INTEGER_KEY