Skip to content

Commit

Permalink
feat(data/set): remove has_neg instance (#367)
Browse files Browse the repository at this point in the history
  • Loading branch information
fpvandoorn committed Jun 29, 2020
1 parent e865d10 commit bdddb70
Showing 1 changed file with 0 additions and 3 deletions.
3 changes: 0 additions & 3 deletions library/init/data/set.lean
Expand Up @@ -66,9 +66,6 @@ instance : has_inter (set α) :=
def compl (s : set α) : set α :=
{a | a ∉ s}

instance : has_neg (set α) :=
⟨compl⟩

protected def diff (s t : set α) : set α :=
{a ∈ s | a ∉ t}

Expand Down

0 comments on commit bdddb70

Please sign in to comment.