Zulip Chat Archive

Stream: general

Topic: has_sub


view this post on Zulip Kevin Buzzard (Jul 19 2019 at 23:19):

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?


Last updated: May 08 2021 at 03:17 UTC