refactor(library/init): change subtype notation and put it on the top-level

library/data/nat/bquant.lean

@@ -23,7 +23,7 @@ namespace nat
   ∃ x, x < n ∧ P x
 
   definition bsub [reducible] (n : nat) (P : nat → Prop) : Type₁ :=
-  {x | x < n ∧ P x}
+  {x \ x < n ∧ P x}
 
   definition ball [reducible] (n : nat) (P : nat → Prop) : Prop :=
   ∀ x, x < n → P x
@@ -127,13 +127,13 @@ namespace nat
   variable [decP : decidable_pred P]
   include decP
 
-  definition bsub_not_of_not_ball : ∀ {n : nat}, ¬ ball n P → {i | i < n ∧ ¬ P i}
+  definition bsub_not_of_not_ball : ∀ {n : nat}, ¬ ball n P → {i \ i < n ∧ ¬ P i}
   | 0        h := absurd (ball_zero P) h
   | (succ n) h := decidable.by_cases
     (λ hp : P n,
       have ¬ ball n P, from
         assume b : ball n P, absurd (ball_succ_of_ball b hp) h,
-      have {i | i < n ∧ ¬ P i}, from bsub_not_of_not_ball this,
+      have {i \ i < n ∧ ¬ P i}, from bsub_not_of_not_ball this,
       bsub_succ this)
     (λ hn : ¬ P n, bsub_succ_of_pred hn)
 

library/data/nat/find.lean

@@ -95,7 +95,7 @@ lt.by_cases
 private lemma wf_gtb : well_founded gtb :=
 well_founded.intro acc_of_ex
 
-private definition find.F (x : nat) : (Π x₁, x₁ ≺ x → lbp x₁ → {a : nat | p a}) → lbp x → {a : nat | p a} :=
+private definition find.F (x : nat) : (Π x₁, x₁ ≺ x → lbp x₁ → {a : nat \ p a}) → lbp x → {a : nat \ p a} :=
 match x with
 | 0 := λ f l0, by_cases
   (λ p0 : p 0,    tag 0 p0)
@@ -111,7 +111,7 @@ match x with
     f (succ (succ n)) this lss)
 end
 include ex -- todo remove
-private definition find_x : {x : nat | p x} :=
+private definition find_x : {x : nat \ p x} :=
 @fix _ _ _ wf_gtb find.F 0 lbp_zero
 end find_x
 

library/init/classical.lean

@@ -14,13 +14,13 @@ open subtype
 -- In the presence of classical logic, we could prove this from a weaker statement:
 -- axiom indefinite_description {A : Type} {P : A->Prop} (H : ∃x, P x) : {x : A, P x}
 axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A) :
-  { x | (∃y : A, P y) → P x}
+  { x \ (∃y : A, P y) → P x}
 
 theorem exists_true_of_nonempty {A : Type} (H : nonempty A) : ∃x : A, true :=
 nonempty.elim H (take x, exists.intro x trivial)
 
 noncomputable definition inhabited_of_nonempty {A : Type} (H : nonempty A) : inhabited A :=
-let u : {x | (∃y : A, true) → true} := strong_indefinite_description (λa, true) H in
+let u : {x \ (∃y : A, true) → true} := strong_indefinite_description (λa, true) H in
 inhabited.mk (elt_of u)
 
 noncomputable definition inhabited_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
@@ -29,13 +29,13 @@ inhabited_of_nonempty (exists.elim H (λ w Hw, nonempty.intro w))
 /- the Hilbert epsilon function -/
 
 noncomputable definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A :=
-let u : {x | (∃y, P y) → P x} :=
+let u : {x \ (∃y, P y) → P x} :=
   strong_indefinite_description P H in
 elt_of u
 
 theorem epsilon_spec_aux {A : Type} (H : nonempty A) (P : A → Prop) (Hex : ∃y, P y) :
     P (@epsilon A H P) :=
-let u : {x | (∃y, P y) → P x} :=
+let u : {x \ (∃y, P y) → P x} :=
   strong_indefinite_description P H in
 have aux : (∃y, P y) → P (elt_of (strong_indefinite_description P H)), from has_property u,
 aux Hex

library/init/instances.lean

@@ -8,7 +8,7 @@ import init.meta.mk_dec_eq_instance init.subtype init.meta.occurrences
 
 open tactic subtype
 
-definition subtype_decidable_eq [instance] {A : Type} {P : A → Prop} [decidable_eq A] : decidable_eq {x | P x} :=
+definition subtype_decidable_eq [instance] {A : Type} {P : A → Prop} [decidable_eq A] : decidable_eq {x \ P x} :=
 by mk_dec_eq_instance
 
 definition list_decidable_eq [instance] {A : Type} [decidable_eq A] : decidable_eq (list A) :=

library/init/subtype.lean

@@ -12,10 +12,11 @@ set_option structure.proj_mk_thm true
 structure subtype {A : Type} (P : A → Prop) :=
 tag :: (elt_of : A) (has_property : P elt_of)
 
-namespace subtype
-  notation `{` binder ` | ` r:(scoped:1 P, subtype P) `}` := r
+notation `{` binder ` \ `:0 r:(scoped:1 P, subtype P) `}` := r
 
-  definition exists_of_subtype {A : Type} {P : A → Prop} : { x | P x } → ∃ x, P x
+namespace subtype
+
+  definition exists_of_subtype {A : Type} {P : A → Prop} : { x \ P x } → ∃ x, P x
   | (subtype.tag a h) := exists.intro a h
 
   variables {A : Type} {P : A → Prop}
@@ -26,12 +27,12 @@ namespace subtype
   theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 :=
   eq.subst H3 (tag_irrelevant H1) H2
 
-  protected theorem eq : ∀ {a1 a2 : {x | P x}} (H : elt_of a1 = elt_of a2), a1 = a2
+  protected theorem eq : ∀ {a1 a2 : {x \ P x}} (H : elt_of a1 = elt_of a2), a1 = a2
   | (tag x1 H1) (tag x2 H2) := tag_eq
 end subtype
 
 open subtype
 
 variables {A : Type} {P : A → Prop}
-protected definition subtype.is_inhabited [instance] {a : A} (H : P a) : inhabited {x | P x} :=
+protected definition subtype.is_inhabited [instance] {a : A} (H : P a) : inhabited {x \ P x} :=
 inhabited.mk (tag a H)