diff --git a/tests/lean/simplifier19.lean b/tests/lean/simplifier19.lean new file mode 100644 index 000000000..ced40ce92 --- /dev/null +++ b/tests/lean/simplifier19.lean @@ -0,0 +1,12 @@ +-- Nested fusion +import algebra.simplifier +open algebra + +universe l +constants (T : Type.{l}) (s : algebra.comm_ring T) +constants (x1 x2 x3 x4 : T) (f g : T → T) +attribute s [instance] +set_option simplify.max_steps 50000 +set_option simplify.fuse true + +#simplify eq simplifier.som 0 f (x1 * x2 * 3 * 4 - 4 * 3 * x1 * x2) + g (x1 * x2 * 3 * 4 - 4 * 3 * x1 * x2) diff --git a/tests/lean/simplifier19.lean.expected.out b/tests/lean/simplifier19.lean.expected.out new file mode 100644 index 000000000..e28be4f53 --- /dev/null +++ b/tests/lean/simplifier19.lean.expected.out @@ -0,0 +1 @@ +g 0 + f 0