RE: Promotion of bare decorations & comparisons

["Nathan T. Hayes" <nh@xxxxxxxxxxxxxxxxx>]

Jurgen Wolff von Gudenberg wrote:
> > 	-- certain comparison relations on bare decorations such as [1,2]
> > \subseteq def will always be true, and this seems very dangerous to me
> bare decorations are dangerous, (hence they are optional)
> the interpretation of DEF as an arbitrary nonempty interval is more
> natural IMO than as Empty. "there is ab interval X so that [1,2]
> \subseteq X"

Using compressed interval arithmetic I get, for example:

	[1,2] \subseteq floor([5,6])
		= [1,2] \subseteq ([5,6],def) // decorated result
		= [1,2] \subseteq def // compress decorated result (throw
away interval part)
		= [1,2] \subseteq Entire // promote def to Entire for
comparison
		= true

That is a false positive, no?

IMO, it is much better to have the bare decoration promote to Empty to avoid
this situation.

Nate