Re: Larch "oversight"
I do recall seeing your short note to comp.spec.larch. In fact, I
actually saved a copy. I apologize for not responding to it at the time.
In my reading, your trait
forall x, y, z:Two
(x = y or x = z) or y = z
is illegal because Two does not belong to its sort set, which is empty.
... whatever ...
AtMostTwo(T for Two)
is also illegal, because it implies an illegal trait.
Is it an oversight or a feature that the definition of the sort set
of a trait excludes Two from the sort set of AtMostTwo? I'm not sure
what the original authors of LSL (John Guttag and Jim Horning) would say.
I've never been completely happy that the sort set is defined implicitly
by the operator set, and would have preferred to see explicit and separate
"declare sorts", "declare operators", and "declare variables" sections as
there are in LP.