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