has_sub

Stream: general

[Kevin Buzzard]

instance notation.sub_eq_add_neg (X : Type) [has_add X] [has_neg X] :
has_sub X := ⟨λ a b, a + -b⟩

class has_field_notation (X : Type) extends has_zero X, has_one X,
has_mul X, has_add X, has_neg X -- note: don't use has_sub
-- because it might cause a diamond now

Some cool notation hacks. What do you think?