[Question][Hw4] Usage and meaning of order

[qawbecrdtey]

In each modules Sign and Interval, there are functions order and cmp. I believe cmp is for comparison between integers and order is for ordering between abstract elements. However, I couldn't figure out what the output should be if two elements are not in a single chain.

[KihongHeo]

It is obviously the same as the following definition: if the two elements are ordered, then true. Otherwise false.

[qawbecrdtey]

So does it mean order x y is true if and only if they are on a same chain, regardless of their order x <= y or x >= y?

[KihongHeo]

order x y iff $x \sqsubseteq y$.

[qawbecrdtey]

Thank you for the reply!