Zulip Chat Archive

Stream: maths

Topic: finset.inter


view this post on Zulip Kevin Buzzard (Feb 16 2020 at 16:12):

import data.finset

/-
From data.finset:

/-- `s ∩ t` is the set such that `a ∈ s ∩ t` iff `a ∈ s` and `a ∈ t`. -/
instance : has_inter (finset α) := ⟨λ s₁ s₂, ⟨_, nodup_ndinter s₂.1 s₁.2⟩⟩

-/

instance (X : Type*) : has_inter (finset X) := by apply_instance -- fails

Why can't I intersect finite sets?

view this post on Zulip Chris Hughes (Feb 16 2020 at 16:12):

decidable equality

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 16:13):

rofl

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 16:13):

thanks again

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 16:14):

PS I'd just got there myself -- the annoying part is guessing the name of the instance because it's never explicitly named in mathlib. Could the name of the instance be put in the comments or is that crazy?

view this post on Zulip Kevin Buzzard (Feb 16 2020 at 16:14):

It wasn't hard to guess this time, but it's the only way I know of debugging these things

view this post on Zulip Floris van Doorn (Feb 17 2020 at 20:53):

You can run #print instances has_inter to find the name.


Last updated: May 14 2021 at 19:21 UTC