Eric Botcazou <ebotca...@adacore.com> writes: >> Yeah. E.g. for ==, the two options would be: >> >> a) must_eq (a, b) -> a == b >> must_ne (a, b) -> a != b >> >> which has the weird property that (a == b) != (!(a != b)) >> >> b) must_eq (a, b) -> a == b >> may_ne (a, b) -> a != b >> >> which has the weird property that a can be equal to b when a != b > > Yes, a) was the one I had in mind, i.e. the traditional operators are the > must > variants and you use an outer ! in order to express the may. Of course this > would require a bit of discipline but, on the other hand, if most of the > cases > fall in the must category, that could be less ugly.
I just think that discipline is going to be hard to maintain in practice, since it's so natural to assume (a == b || a != b) == true. With the may/must approach, static type checking forces the issue. >> Sorry about that. It's the best I could come up with without losing >> the may/must distinction. > > Which variant is known_zero though? Must or may? must. maybe_nonzero is the may version. Thanks, Richard
