fix(library/data/{set,finset}/basic.lean: delete \{{ \}}} notation (conflicts with records)

This commit is contained in:
Jeremy Avigad 2015-05-16 17:47:31 +10:00
parent d4da381e1a
commit 81d0d4aa53
2 changed files with 4 additions and 7 deletions

View file

@ -145,7 +145,7 @@ quot.lift_on s
-- set builder notation
notation `{[`:max a:(foldr `,` (x b, insert x b) ∅) `]}`:0 := a
notation `⦃` a:(foldr `,` (x b, insert x b) ∅) `⦄` := a
-- notation `⦃` a:(foldr `,` (x b, insert x b) ∅) `⦄` := a
theorem mem_insert (a : A) (s : finset A) : a ∈ insert a s :=
quot.induction_on s
@ -165,7 +165,7 @@ propext (iff.intro
(assume H' : x = a, eq.subst (eq.symm H') !mem_insert)
(assume H' : x ∈ s, !mem_insert_of_mem H')))
theorem insert_empty_eq (a : A) : ⦃a⦄ = singleton a := rfl
theorem insert_empty_eq (a : A) : {[ a ]} = singleton a := rfl
theorem insert_eq_of_mem {a : A} {s : finset A} (H : a ∈ s) : insert a s = s :=
ext
@ -306,7 +306,7 @@ ext (take x,
x ∈ insert a s ↔ x ∈ insert a s : iff.refl
... = (x = a x ∈ s) : mem_insert_eq
... = (x ∈ singleton a x ∈ s) : mem_singleton_eq
... = (x ∈ ⦃a⦄ s) : mem_union_eq)
... = (x ∈ {[ a ]} s) : mem_union_eq)
theorem insert_union (a : A) (s t : finset A) : insert a (s t) = insert a s t :=
by rewrite [*insert_eq, union.assoc]

View file

@ -1,8 +1,6 @@
/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: data.set.basic
Author: Jeremy Avigad, Leonardo de Moura
-/
import logic
@ -126,10 +124,9 @@ notation `{` binders `|` r:(scoped:1 P, set_of P) `}` := r
definition filter (P : X → Prop) (s : set X) : set X := λx, x ∈ s ∧ P x
notation `{` binders ∈ s `|` r:(scoped:1 p, filter p s) `}` := r
-- {[x, y, z]} or ⦃x, y, z⦄
-- {[x, y, z]}
definition insert (x : X) (a : set X) : set X := {y : X | y = x y ∈ a}
notation `{[`:max a:(foldr `,` (x b, insert x b) ∅) `]}`:0 := a
notation `⦃` a:(foldr `,` (x b, insert x b) ∅) `⦄` := a
/- set difference -/