subtype example backwards? #197
Description
I've recently retired, and hope to use Z3 for a project. So I'm trying to catch up on this amazing tool. In the process, I was reading https://microsoft.github.io/z3guide/docs/logic/Quantifiers#effectively-propositional, and I got confused. It says:
The following example axiomatizes a subtype partial order relation that has the tree property. That is, if x and y are subtypes of z, then x is a subtype of y or y is a subtype of x.
I understand the term "subtype" to mean that in a language with single inheritance, if B inherits from A, then B is a (proper) subtype of A, and A is a supertype of B. So I think this sentence (and the example that follows it) is reversed -- it would make sense if you substituted "supertype" for "subtype". To make this point clearly, if B1 and B2 both inherit from A, then they are both subtypes of A, but neither of B1 or B2 are subtypes (or supertypes) of the other.