3 ms·
I think it lines up with OR in the sense that x:(S+T) <==> x:S OR x:T If you know x:S you may find conclude x:(S+T) without also stipulating that x is not a T
by abeppu 2y ago
I think it lines up with OR in the sense that
x:(S+T) <==> x:S OR x:T
If you know x:S you may find conclude x:(S+T) without also stipulating that x is not a T. It may be permitted (if pointless) to use S+T even in contexts where S is a subtype of T (and hence the XOR is not true).
- ndriscoll 2y agoOR and XOR are both "wrong". It's a disjoint union. T+T = 2T, not T or 0. When S and T are disjoint, then it's OR-like (and also XOR-like). You can't conclude x: S+T from x:S (because it's false). What you can do is use x to build an S+T. If S=T there are two ways to do that. From what I've seen, usually subtyping is also defined via embeddings, and if x: T then x: S is false for all S != T by definition.