On Tue, Oct 24, 2017 at 1:23 PM, Richard Sandiford <richard.sandif...@linaro.org> wrote: > 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.
Can you rename known_zero to must_be_zero then? What's wrong with must_eq (X, 0) / may_eq (X, 0) btw? Richard. > Thanks, > Richard
