2015-11-16 08:54:21 -08:00
|
|
|
-- normalizing reducible non-subsingleton instances
|
2015-12-04 17:57:03 -08:00
|
|
|
import algebra.ring
|
2015-11-16 08:54:21 -08:00
|
|
|
open algebra
|
|
|
|
|
|
|
|
|
|
universe l
|
2015-12-05 23:52:16 -08:00
|
|
|
constants (T : Type.{l}) (s : comm_ring T)
|
2015-11-16 08:54:21 -08:00
|
|
|
constants (x1 x2 x3 x4 : T) (f g : T → T)
|
|
|
|
|
attribute s [instance]
|
|
|
|
|
|
|
|
|
|
set_option pp.all true
|
|
|
|
|
|
|
|
|
|
#simplify eq null 0 x1
|
|
|
|
|
#simplify eq null 0 x1 + x1
|
|
|
|
|
#simplify eq null 0 x1 + x1 + x1
|
|
|
|
|
#simplify eq null 0 x1 + x1 + x1 + x1
|
|
|
|
|
#simplify eq null 0 x1 + x1 + (x1 + x1) + x1
|
|
|
|
|
#simplify eq simplifier.ac 0 x1 + x1 + x1
|
|
|
|
|
#simplify eq simplifier.ac 0 x1 + x1 + x1 + x1
|
|
|
|
|
#simplify eq simplifier.ac 0 x1 + x1 + (x1 + x1) + x1
|
