6 | ||| When normalizing arithmetic expressions, we must
7 | ||| make sure that factors that evaluate to zero must
8 | ||| be removed from the sum of products.
9 | |||
10 | ||| For instance, the following example only works,
11 | ||| if the term `0 * x * y` gets removed before comparing
12 | ||| the normalized sums:
13 | |||
14 | ||| ```idris example
15 | ||| 0 binom3 : {x,y : Bits8} -> (x + y) * (x - y) === x * x - y * y
16 | ||| binom3 = solve [x,y] ((x .+. y) * (x .-. y)) (x .*. x - y .*. y)
17 | ||| ```
18 | |||
19 | ||| Because we cannot directly use a (primitive) pattern match
20 | ||| without having a concrete type, we need this interface.
21 | ||| (We *could* use `DecEq`, but this is not publicly exported
22 | ||| for the primitives; probably for good reasons since it is
23 | ||| implemented using `believe_me`).
27 | ||| Checks if a value is propositionally equal to zero.