1 Jan
2015
1 Jan
'15
9:18 a.m.
On Thu, Jan 01, 2015 at 02:14:16PM +0000, Tom Ellis wrote:
So let me clarify that I want (<=) to be a total order in the sense that it is
* reflexive * symmetric * transitive
and `(x <= y) && (y <= x)` implies that `x == y`. (*)
Correction: I mean "antisymmetric" not "symmetric". Anti-symmetry is exactly this condition (*). Futhermore I want (==) to be at least as fine-grained as extensional equivalence. Tom