When normalizing arithmetic expressions, we must
make sure that factors that evaluate to zero must
be removed from the sum of products.
For instance, the following example only works,
if the term `0 * x * y` gets removed before comparing
the normalized sums:
```idris example
0 binom3 : {x,y : Bits8} -> (x + y) * (x - y) === x * x - y * y
binom3 = solve [x,y] ((x .+. y) * (x .-. y)) (x .*. x - y .*. y)
```
Because we cannot directly use a (primitive) pattern match
without having a concrete type, we need this interface.
(We *could* use `DecEq`, but this is not publicly exported
for the primitives; probably for good reasons since it is
implemented using `believe_me`).
Parameters: a
Constraints: Ring a
Methods:
isZero : (v : a) -> Maybe (v = 0) Checks if a value is propositionally equal to zero.
Implementations:
SolvableRing Bits8SolvableRing Bits16SolvableRing Bits32SolvableRing Bits64SolvableRing Int8SolvableRing Int16SolvableRing Int32SolvableRing Int64SolvableRing IntSolvableRing Integer