Skip to content

Possible mistake in `la_generic` definition

In the specification for the la_generic rule, when describing how to sum the processed inequalities, the spec says this:

The operator ⋈ is ≈ if all operators are ≈, > if all are either ≈ or >, and ≥ otherwise.

This implies that, if we have one > operator and one \geq, the resulting operator should be \geq. However, I believe in this case the operator should be > (intuitively, if we have a > b and c \geq d, we can infer that a + c > b + d). I propose the correct definition should be:

The operator ⋈ is ≈ if all operators are ≈, ≥ if all are either ≈ or ≥, and > otherwise.

This mistake does not affect the correctness of the rule, since a > b \rightarrow a \geq b, but fixing it would allow more valid applications.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information