instance

Stream: new members

[Nicolò Cavalleri]

I can't locate this instance in the library:

example {α : Type*} {β : Type*} [group β] : group α → β := by library_search

Is library_search supposed to find instances as well?

[Alex J. Best]

Are the brackets right?

[Markus Himmel]

They aren't:

import algebra.pi_instances

example {α : Type*} {β : Type*} [group β] : group (α → β) := by library_search -- Try this: refine pi.group

[Nicolò Cavalleri]

Ok it did not really come to my mind that the priority could have been greater for group than for the arrow.
Since you're here, regarding this instance, what is the dollar here?

@[to_additive add_group]
instance group [∀ i, group $ f i] : group (Π i : I, f i) :=
by refine_struct { one := (1 : Π i, f i), mul := (*), inv := has_inv.inv, .. };
  tactic.pi_instance_derive_field

I think the dollar is never mentioned in the online book...

[Alex J. Best]

$ means bracket everything to the right, so its equivalent to [∀ i, group (f i)] here, it can be helpful with long lines with lots of brackets

[Jalex Stark]

a $ b is like a ( b )

[Nicolò Cavalleri]

Ok thanks a lot!

[Vaibhav Karve]

Another instance-related question:
Should band and bor be instances of is_associative and is_commutative? I couldn't find it in mathlib. The closest thing is bool.bor_comm etc. which is listed here: https://leanprover-community.github.io/mathlib_docs/data/bool.html