michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(simplifier19): nested fusion

Browse source
This commit is contained in:
Daniel Selsam 2015-11-16 20:32:14 -08:00
parent 2eeab1c757
commit 835e8995b4
2 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/simplifier19.lean Normal file
View file

@ -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)

1
tests/lean/simplifier19.lean.expected.out Normal file
View file

@ -0,0 +1 @@
g 0 + f 0