finset.inter

Stream: maths

[Kevin Buzzard]

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?

[Chris Hughes]

decidable equality

[Kevin Buzzard]

rofl

[Kevin Buzzard]

thanks again

[Kevin Buzzard]

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?

[Kevin Buzzard]

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

[Floris van Doorn]

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