> does numerical destructing require that one of the terms be a constant?

Yes, the general pattern is `n + K`. I'm looking to expanding this to other operations in the future too.

> Did you mean arg -> f ?

Yes. I changed the syntax recently, but forgot to change the README. Thanks for pointing this out!

> 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.

I think my other answer here should provide an answer: https://news.ycombinator.com/item?id=31989227

Ah, that makes sense. Thanks!