indexing
	description: "Truth values, with the boolean operations"

expanded class interface
	BOOLEAN

feature -- Access

	hash_code: INTEGER
			-- Hash code value
			-- (from BOOLEAN_REF)
		ensure -- from HASHABLE
			good_hash_value: Result >= 0

	item: BOOLEAN
			-- Boolean value
			-- (from BOOLEAN_REF)
	
feature -- Status report

	is_hashable: BOOLEAN
			-- May current object be hashed?
			-- (True if it is not its type's default.)
			-- (from BOOLEAN_REF)
		ensure -- from HASHABLE
			ok_if_not_default: Result implies (Current /= default)
	
feature -- Element change

	set_item (b: BOOLEAN)
			-- Make b the item value.
			-- (from BOOLEAN_REF)
	
feature -- Basic operations

	infix "and" (other: like Current): BOOLEAN
			-- Boolean conjunction with other
			-- (from BOOLEAN_REF)
		require -- from BOOLEAN_REF
			other_exists: other /= void
		ensure -- from BOOLEAN_REF
			de_morgan: Result = not (not Current or not other);
			commutative: Result = (other and Current);
			consistent_with_semi_strict: Result implies (Current and then other)

	infix "and then" (other: like Current): BOOLEAN
			-- Boolean semi-strict conjunction with other
			-- (from BOOLEAN_REF)
		require -- from BOOLEAN_REF
			other_exists: other /= void
		ensure -- from BOOLEAN_REF
			de_morgan: Result = not (not Current or else not other)

	infix "implies" (other: like Current): BOOLEAN
			-- Boolean implication of other
			-- (semi-strict)
			-- (from BOOLEAN_REF)
		require -- from BOOLEAN_REF
			other_exists: other /= void
		ensure -- from BOOLEAN_REF
			definition: Result = (not Current or else other)

	prefix "not ": like Current
			-- Negation
			-- (from BOOLEAN_REF)

	infix "or" (other: like Current): BOOLEAN
			-- Boolean disjunction with other
			-- (from BOOLEAN_REF)
		require -- from BOOLEAN_REF
			other_exists: other /= void
		ensure -- from BOOLEAN_REF
			de_morgan: Result = not (not Current and not other);
			commutative: Result = (other or Current);
			consistent_with_semi_strict: Result implies (Current or else other)

	infix "or else" (other: like Current): BOOLEAN
			-- Boolean semi-strict disjunction with other
			-- (from BOOLEAN_REF)
		require -- from BOOLEAN_REF
			other_exists: other /= void
		ensure -- from BOOLEAN_REF
			de_morgan: Result = not (not Current and then not other)

	infix "xor" (other: like Current): BOOLEAN
			-- Boolean exclusive or with other
			-- (from BOOLEAN_REF)
		require -- from BOOLEAN_REF
			other_exists: other /= void
		ensure -- from BOOLEAN_REF
			definition: Result = ((Current or other) and not (Current and other))
	
feature -- Output

	out: STRING
			-- Printable representation of boolean
			-- (from BOOLEAN_REF)
	
invariant

		-- from GENERAL
	reflexive_equality: standard_is_equal (Current);
	reflexive_conformance: conforms_to (Current);
		-- from BOOLEAN_REF
	involutive_negation: is_equal (not (not Current));
	non_contradiction: not (Current and (not Current));
	completeness: Current or else (not Current);

end -- class BOOLEAN