Stream: new members

Topic: instance

Nicolò Cavalleri (Jul 14 2020 at 15:35):

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 (Jul 14 2020 at 15:38):

Are the brackets right?

Markus Himmel (Jul 14 2020 at 15:38):

They aren't:

import algebra.pi_instances

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


Nicolò Cavalleri (Jul 14 2020 at 15:43):

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]

Jalex Stark (Jul 14 2020 at 15:44):

a \$ b is like a ( b )

Ok thanks a lot!

Vaibhav Karve (Jul 14 2020 at 18:14):

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

Last updated: May 14 2021 at 04:22 UTC