> Yes, the general pattern is `n + K`. OK, so what is the intended benefit of y ~ x + 1 over x = y - 1 ? I can see an obvious benefit if I can write y ~ x + z

> Yes, the general pattern is `n + K`. OK, so what is the intended benefit of y ~ x + 1 over x = y - 1 ? I can see an obvious benefit if I can write y ~ x + z where neither x nor z is a constant and the resulting semantics invoke some kind of mathematical constraint management system or backtracking search a la Prolog, but if I'm constrained to write things that can be trivially transformed into a binding I don't see the point.