Zulip Chat Archive

Stream: new members

Topic: instance


view this post on Zulip 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?

view this post on Zulip Alex J. Best (Jul 14 2020 at 15:38):

Are the brackets right?

view this post on Zulip 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

view this post on Zulip 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]
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...

view this post on Zulip Alex J. Best (Jul 14 2020 at 15:44):

$ 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

view this post on Zulip Jalex Stark (Jul 14 2020 at 15:44):

a $ b is like a ( b )

view this post on Zulip Nicolò Cavalleri (Jul 14 2020 at 15:44):

Ok thanks a lot!

view this post on Zulip 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