deferred class
	INTEGER_NUMBER

inherit
	REAL_NUMBER
		rename
			value as real_value,
			equals as real_equals,
			opposite as real_opposite,
			normalized_value as real_normalized_value
		end

feature -- Primitive

	value: INTEGER
			-- Native value of current integer number
		deferred
		end

feature -- Access

	zero: like integer_anchor
			-- The integer number 0
		deferred
		end

feature -- Factory

	normalized_value (v: INTEGER): INTEGER
			-- `v' adapted to represent the `value' of current integer number
		deferred
		ensure
			stable: normalized_value (Result) = Result
		end

invariant
	value: value.to_real = real_value

end
