Constrain unique number types when doing range arithmetic

[kevinbarabash]

If you have an array of length N. Its keys could be represented by the range 0..N where the upper limit is non-inclusive. If you have a range 0..N-1 it's trivial to show that this range is fully contained within 0..N. In order for 0..N-1 to be a valid range though, N must be at least 1. This information should allow a person to prove that (0..N-1) + 1 is also inside 0..N. I just need to figure out to prove that. 😓

now that binary types support comparison operators, the constraints could just be other types like they are in regular type params/variables 🙂

• https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
• https://pkg.go.dev/github.com/google/wuffs/lib/interval
• https://github.com/Z3Prover/z3

[kevinbarabash]

It's almost like unique symbol and unique number types appearing in a function signature need to be generalized somehow so that when the function is called a new unique symbol or unique number is returned.