HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Arithmetic normalisation involving two subtractions fails if either can't be moved

Open mn200 opened this issue 5 years ago • 0 comments

Viz:

> SIMP_CONV (srw_ss() ++ numSimps.ARITH_ss) [] ``n2 + (fxx - 1) + 1 - n2``;
Exception- UNCHANGED raised

The n2's should be cancelled even though the -1 can't be moved out from under the fxx.

mn200 avatar Mar 04 '19 23:03 mn200