From b7abd615798b025ece3203b1065529f25dfec665 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 21 Sep 2016 16:59:42 -0700
Subject: [PATCH] feat(frontends/lean): change subtype notation (again)

We had conflicts with the set notation.
---
 library/init/classical.lean                 | 134 ++++++++++----------
 library/init/coe.lean                       |   2 +-
 library/init/instances.lean                 |   2 +-
 library/init/subtype.lean                   |   6 +-
 src/frontends/lean/brackets.cpp             |   8 +-
 src/frontends/lean/pp.cpp                   |   2 +-
 src/frontends/lean/token_table.cpp          |   2 +-
 src/frontends/lean/tokens.cpp               |   8 +-
 src/frontends/lean/tokens.h                 |   2 +-
 src/frontends/lean/tokens.txt               |   2 +-
 tests/lean/curly_notation.lean              |   9 ++
 tests/lean/curly_notation.lean.expected.out |   4 +
 tests/lean/print_ax1.lean.expected.out      |   2 +-
 tests/lean/print_ax2.lean.expected.out      |   2 +-
 tests/lean/print_ax3.lean.expected.out      |   2 +-
 tests/lean/run/cute_binders.lean            |   4 -
 tests/lean/run/match2.lean                  |   2 +-
 tests/lean/run/set.lean                     |   7 -
 tests/lean/run/set2.lean                    |  19 ---
 tests/lean/run/sub.lean                     |   5 +-
 tests/lean/run/sub_bug.lean                 |   2 +-
 tests/lean/struct_class.lean.expected.out   |   6 +
 tests/lean/subpp.lean                       |   4 +-
 tests/lean/subpp.lean.expected.out          |   2 +-
 24 files changed, 112 insertions(+), 126 deletions(-)
 delete mode 100644 tests/lean/run/set.lean
 delete mode 100644 tests/lean/run/set2.lean

diff --git a/library/init/classical.lean b/library/init/classical.lean
index 426712d73d..33d2f56a61 100644
--- a/library/init/classical.lean
+++ b/library/init/classical.lean
@@ -11,58 +11,58 @@ universe variables u v
 /- the axiom -/
 
 -- In the presence of classical logic, we could prove this from a weaker statement:
--- axiom indefinite_description {A : Type u} {P : A->Prop} (H : ∃ x, P x) : {x : A, P x}
-axiom strong_indefinite_description {A : Type u} (P : A → Prop) (H : nonempty A) :
-  { x \ (∃ y : A, P y) → P x}
+-- axiom indefinite_description {A : Type u} {p : A->Prop} (H : ∃ x, p x) : {x : A, p x}
+axiom strong_indefinite_description {A : Type u} (p : A → Prop) (H : nonempty A) :
+  { x : A // (∃ y : A, p y) → p x}
 
-theorem exists_true_of_nonempty {A : Type u} (H : nonempty A) : ∃ x : A, true :=
-nonempty.elim H (take x, ⟨x, trivial⟩)
+theorem exists_true_of_nonempty {A : Type u} (h : nonempty A) : ∃ x : A, true :=
+nonempty.elim h (take x, ⟨x, trivial⟩)
 
-noncomputable definition inhabited_of_nonempty {A : Type u} (H : nonempty A) : inhabited A :=
-⟨elt_of (strong_indefinite_description (λ a, true) H)⟩
+noncomputable definition inhabited_of_nonempty {A : Type u} (h : nonempty A) : inhabited A :=
+⟨elt_of (strong_indefinite_description (λ a, true) h)⟩
 
-noncomputable definition inhabited_of_exists {A : Type u} {P : A → Prop} (H : ∃ x, P x) : inhabited A :=
+noncomputable definition inhabited_of_exists {A : Type u} {p : A → Prop} (H : ∃ x, p x) : inhabited A :=
 inhabited_of_nonempty (exists.elim H (λ w Hw, ⟨w⟩))
 
 /- the Hilbert epsilon function -/
 
-noncomputable definition epsilon {A : Type u} [H : nonempty A] (P : A → Prop) : A :=
-elt_of (strong_indefinite_description P H)
+noncomputable definition epsilon {A : Type u} [h : nonempty A] (p : A → Prop) : A :=
+elt_of (strong_indefinite_description p h)
 
-theorem epsilon_spec_aux {A : Type u} (H : nonempty A) (P : A → Prop) (Hex : ∃ y, P y) :
-    P (@epsilon A H P) :=
-have aux : (∃ y, P y) → P (elt_of (strong_indefinite_description P H)), from has_property (strong_indefinite_description P H),
-aux Hex
+theorem epsilon_spec_aux {A : Type u} (h : nonempty A) (p : A → Prop) (hex : ∃ y, p y) :
+    p (@epsilon A h p) :=
+have aux : (∃ y, p y) → p (elt_of (strong_indefinite_description p h)), from has_property (strong_indefinite_description p h),
+aux hex
 
-theorem epsilon_spec {A : Type u} {P : A → Prop} (Hex : ∃ y, P y) :
-    P (@epsilon A (nonempty_of_exists Hex) P) :=
-epsilon_spec_aux (nonempty_of_exists Hex) P Hex
+theorem epsilon_spec {A : Type u} {p : A → Prop} (hex : ∃ y, p y) :
+    p (@epsilon A (nonempty_of_exists hex) p) :=
+epsilon_spec_aux (nonempty_of_exists hex) p hex
 
 theorem epsilon_singleton {A : Type u} (a : A) : @epsilon A ⟨a⟩ (λ x, x = a) = a :=
 @epsilon_spec A (λ x, x = a) ⟨a, rfl⟩
 
-noncomputable definition some {A : Type u} {P : A → Prop} (H : ∃ x, P x) : A :=
-@epsilon A (nonempty_of_exists H) P
+noncomputable definition some {A : Type u} {p : A → Prop} (h : ∃ x, p x) : A :=
+@epsilon A (nonempty_of_exists h) p
 
-theorem some_spec {A : Type u} {P : A → Prop} (H : ∃ x, P x) : P (some H) :=
-epsilon_spec H
+theorem some_spec {A : Type u} {p : A → Prop} (h : ∃ x, p x) : p (some h) :=
+epsilon_spec h
 
 /- the axiom of choice -/
 
-theorem axiom_of_choice {A : Type u} {B : A → Type v} {R : Π x, B x → Prop} (H : ∀ x, ∃ y, R x y) :
+theorem axiom_of_choice {A : Type u} {B : A → Type v} {R : Π x, B x → Prop} (h : ∀ x, ∃ y, R x y) :
   ∃ (f : Π x, B x), ∀ x, R x (f x) :=
-have H : ∀ x, R x (some (H x)), from take x, some_spec (H x),
-⟨_, H⟩
+have h : ∀ x, R x (some (h x)), from take x, some_spec (h x),
+⟨_, h⟩
 
-theorem skolem {A : Type u} {B : A → Type v} {P : Π x, B x → Prop} :
-  (∀ x, ∃ y, P x y) ↔ ∃ (f : Π x, B x) , (∀ x, P x (f x)) :=
+theorem skolem {A : Type u} {B : A → Type v} {p : Π x, B x → Prop} :
+  (∀ x, ∃ y, p x y) ↔ ∃ (f : Π x, B x) , (∀ x, p x (f x)) :=
 iff.intro
-  (assume H : (∀ x, ∃ y, P x y), axiom_of_choice H)
-  (assume H : (∃ (f : Π x, B x), (∀ x, P x (f x))),
-    take x, exists.elim H (λ (fw : ∀ x, B x) (Hw : ∀ x, P x (fw x)),
-      ⟨fw x, Hw x⟩))
+  (assume h : (∀ x, ∃ y, p x y), axiom_of_choice h)
+  (assume h : (∃ (f : Π x, B x), (∀ x, p x (f x))),
+    take x, exists.elim h (λ (fw : ∀ x, B x) (hw : ∀ x, p x (fw x)),
+      ⟨fw x, hw x⟩))
 /-
-Prove excluded middle using Hilbert's choice
+Prove excluded middle using hilbert's choice
 The proof follows Diaconescu proof that shows that the axiom of choice implies the excluded middle.
 -/
 section diaconescu
@@ -82,32 +82,32 @@ epsilon_spec ⟨false, or.inl rfl⟩
 
 private lemma not_uv_or_p : ¬(u = v) ∨ p :=
 or.elim u_def
-  (assume Hut : u = true,
+  (assume hut : u = true,
     or.elim v_def
-      (assume Hvf : v = false,
-        have Hne : ¬(u = v), from eq.symm Hvf ▸ eq.symm Hut ▸ true_ne_false,
-        or.inl Hne)
-      (assume Hp : p, or.inr Hp))
-  (assume Hp : p, or.inr Hp)
+      (assume hvf : v = false,
+        have hne : ¬(u = v), from eq.symm hvf ▸ eq.symm hut ▸ true_ne_false,
+        or.inl hne)
+      (assume hp : p, or.inr hp))
+  (assume hp : p, or.inr hp)
 
 private lemma p_implies_uv : p → u = v :=
-assume Hp : p,
-have Hpred : U = V, from
+assume hp : p,
+have hpred : U = V, from
   funext (take x : Prop,
-    have Hl : (x = true ∨ p) → (x = false ∨ p), from
-      assume A, or.inr Hp,
-    have Hr : (x = false ∨ p) → (x = true ∨ p), from
-      assume A, or.inr Hp,
+    have hl : (x = true ∨ p) → (x = false ∨ p), from
+      assume A, or.inr hp,
+    have hr : (x = false ∨ p) → (x = true ∨ p), from
+      assume A, or.inr hp,
     show (x = true ∨ p) = (x = false ∨ p), from
-      propext (iff.intro Hl Hr)),
-have H' : epsilon U = epsilon V, from Hpred ▸ rfl,
-show u = v, from H'
+      propext (iff.intro hl hr)),
+have h' : epsilon U = epsilon V, from hpred ▸ rfl,
+show u = v, from h'
 
 theorem em : p ∨ ¬p :=
-have H : ¬(u = v) → ¬p, from mt p_implies_uv,
+have h : ¬(u = v) → ¬p, from mt p_implies_uv,
   or.elim not_uv_or_p
-    (assume Hne : ¬(u = v), or.inr (H Hne))
-    (assume Hp : p, or.inl Hp)
+    (assume hne : ¬(u = v), or.inr (h hne))
+    (assume hp : p, or.inl hp)
 end diaconescu
 
 theorem prop_complete (a : Prop) : a = true ∨ a = false :=
@@ -119,23 +119,23 @@ definition eq_true_or_eq_false := prop_complete
 
 section aux
 attribute [elab_as_eliminator]
-theorem cases_true_false (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a :=
+theorem cases_true_false (p : Prop → Prop) (h1 : p true) (h2 : p false) (a : Prop) : p a :=
 or.elim (prop_complete a)
-  (assume Ht : a = true,  eq.symm Ht ▸ H1)
-  (assume Hf : a = false, eq.symm Hf ▸ H2)
+  (assume ht : a = true,  eq.symm ht ▸ h1)
+  (assume hf : a = false, eq.symm hf ▸ h2)
 
-theorem cases_on (a : Prop) {P : Prop → Prop} (H1 : P true) (H2 : P false) : P a :=
-cases_true_false P H1 H2 a
+theorem cases_on (a : Prop) {p : Prop → Prop} (h1 : p true) (h2 : p false) : p a :=
+cases_true_false p h1 h2 a
 
 -- this supercedes by_cases in decidable
-definition by_cases {p q : Prop} (Hpq : p → q) (Hnpq : ¬p → q) : q :=
-or.elim (em p) (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp)
+definition by_cases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
+or.elim (em p) (assume hp, hpq hp) (assume hnp, hnpq hnp)
 
 -- this supercedes by_contradiction in decidable
-theorem by_contradiction {p : Prop} (H : ¬p → false) : p :=
+theorem by_contradiction {p : Prop} (h : ¬p → false) : p :=
 by_cases
-  (assume H1 : p, H1)
-  (assume H1 : ¬p, false.rec _ (H H1))
+  (assume h1 : p, h1)
+  (assume h1 : ¬p, false.rec _ (h h1))
 
 theorem eq_false_or_eq_true (a : Prop) : a = false ∨ a = true :=
 cases_true_false (λ x, x = false ∨ x = true)
@@ -143,13 +143,13 @@ cases_true_false (λ x, x = false ∨ x = true)
   (or.inl rfl)
   a
 
-theorem eq.of_iff {a b : Prop} (H : a ↔ b) : a = b :=
-iff.elim (assume H1 H2, propext (iff.intro H1 H2)) H
+theorem eq.of_iff {a b : Prop} (h : a ↔ b) : a = b :=
+iff.elim (assume h1 h2, propext (iff.intro h1 h2)) h
 
 theorem iff_eq_eq {a b : Prop} : (a ↔ b) = (a = b) :=
 propext (iff.intro
-  (assume H, eq.of_iff H)
-  (assume H, iff.of_eq H))
+  (assume h, eq.of_iff h)
+  (assume h, iff.of_eq h))
 
 lemma eq_false {a : Prop} : (a = false) = (¬ a) :=
 have (a ↔ false) = (¬ a), from propext (iff_false a),
@@ -164,8 +164,8 @@ end aux
 noncomputable definition decidable_inhabited (a : Prop) : inhabited (decidable a) :=
 inhabited_of_nonempty
   (or.elim (em a)
-    (assume Ha, ⟨is_true Ha⟩)
-    (assume Hna, ⟨is_false Hna⟩))
+    (assume ha, ⟨is_true ha⟩)
+    (assume hna, ⟨is_false hna⟩))
 local attribute decidable_inhabited [instance]
 
 noncomputable definition prop_decidable (a : Prop) : decidable a :=
@@ -177,8 +177,8 @@ noncomputable definition type_decidable_eq (A : Type u) : decidable_eq A :=
 
 noncomputable definition type_decidable (A : Type u) : sum A (A → false) :=
 match (prop_decidable (nonempty A)) with
-| (is_true Hp) := sum.inl (inhabited.value (inhabited_of_nonempty Hp))
-| (is_false Hn) := sum.inr (λ a, absurd (nonempty.intro a) Hn)
+| (is_true hp) := sum.inl (inhabited.value (inhabited_of_nonempty hp))
+| (is_false hn) := sum.inr (λ a, absurd (nonempty.intro a) hn)
 end
 
 end classical
diff --git a/library/init/coe.lean b/library/init/coe.lean
index fed1f98bfd..8e1075e66f 100644
--- a/library/init/coe.lean
+++ b/library/init/coe.lean
@@ -125,7 +125,7 @@ definition coe_decidable_eq (b : bool) : decidable (coe b) :=
 show decidable (b = tt), from bool.has_decidable_eq b tt
 
 attribute [instance]
-definition coe_subtype {A : Type u} {P : A → Prop} : has_coe {a \ P a} A :=
+definition coe_subtype {A : Type u} {p : A → Prop} : has_coe {a // p a} A :=
 ⟨λ s, subtype.elt_of s⟩
 
 /- Basic lifts -/
diff --git a/library/init/instances.lean b/library/init/instances.lean
index f1903ad60f..63f64ef0a7 100644
--- a/library/init/instances.lean
+++ b/library/init/instances.lean
@@ -9,7 +9,7 @@ open tactic subtype
 universe variables u v
 
 attribute [instance]
-definition subtype_decidable_eq {A : Type u} {P : A → Prop} [decidable_eq A] : decidable_eq {x \ P x} :=
+definition subtype_decidable_eq {A : Type u} {p : A → Prop} [decidable_eq A] : decidable_eq {x : A // p x} :=
 by mk_dec_eq_instance
 
 set_option trace.app_builder true
diff --git a/library/init/subtype.lean b/library/init/subtype.lean
index 89e632ddf5..e9f06dd398 100644
--- a/library/init/subtype.lean
+++ b/library/init/subtype.lean
@@ -14,7 +14,7 @@ tag :: (elt_of : A) (has_property : p elt_of)
 
 namespace subtype
 
-  definition exists_of_subtype {A : Type u} {p : A → Prop} : { x \ p x } → ∃ x, p x
+  definition exists_of_subtype {A : Type u} {p : A → Prop} : { x // p x } → ∃ x, p x
   | ⟨a, h⟩ := ⟨a, h⟩
 
   variables {A : Type u} {p : A → Prop}
@@ -22,7 +22,7 @@ namespace subtype
   theorem tag_irrelevant {a : A} (h1 h2 : p a) : tag a h1 = tag a h2 :=
   rfl
 
-  protected theorem eq : ∀ {a1 a2 : {x \ p x}}, elt_of a1 = elt_of a2 → a1 = a2
+  protected theorem eq : ∀ {a1 a2 : {x // p x}}, elt_of a1 = elt_of a2 → a1 = a2
   | ⟨x, h1⟩ ⟨.x, h2⟩ rfl := rfl
 
 end subtype
@@ -32,5 +32,5 @@ open subtype
 variables {A : Type u} {p : A → Prop}
 
 attribute [instance]
-protected definition subtype.is_inhabited {a : A} (h : p a) : inhabited {x \ p x} :=
+protected definition subtype.is_inhabited {a : A} (h : p a) : inhabited {x // p x} :=
 ⟨⟨a, h⟩⟩
diff --git a/src/frontends/lean/brackets.cpp b/src/frontends/lean/brackets.cpp
index 666864382b..5fae4fd0ec 100644
--- a/src/frontends/lean/brackets.cpp
+++ b/src/frontends/lean/brackets.cpp
@@ -12,7 +12,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/tokens.h"
 
 namespace lean {
-/* Parse rest of the subtype expression prefix '{' id ':' expr '\' ... */
+/* Parse rest of the subtype expression prefix '{' id ':' expr '\\' ... */
 static expr parse_subtype(parser & p, pos_info const & pos, expr const & local) {
     parser::local_scope scope(p);
     p.add_local(local);
@@ -90,7 +90,7 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
         auto id_pos = p.pos();
         name id     = p.get_name_val();
         p.next();
-        if (p.curr_is_token(get_backslash_tk())) {
+        if (p.curr_is_token(get_dslash_tk())) {
             expr type  = p.save_pos(mk_expr_placeholder(), id_pos);
             expr local = p.save_pos(mk_local(id, type), id_pos);
             p.next();
@@ -99,7 +99,7 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
             p.next();
             expr type  = p.parse_expr();
             expr local = p.save_pos(mk_local(id, type), id_pos);
-            p.check_token_next(get_backslash_tk(), "invalid subtype, '\' expected");
+            p.check_token_next(get_dslash_tk(), "invalid subtype, '//' expected");
             return parse_subtype(p, pos, local);
         } else if (p.curr_is_token(get_period_tk())) {
             p.next();
@@ -132,7 +132,7 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po
         p.next();
         return parse_monadic_comprehension(p, pos, e);
     } else {
-        throw parser_error("invalid '{' expression, ',', '}', 'with', `\\` or `|` expected", p.pos());
+        throw parser_error("invalid '{' expression, ',', '}', 'with', `//` or `|` expected", p.pos());
     }
 }
 }
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 81d920d39d..509085713a 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -1470,7 +1470,7 @@ auto pretty_fn::pp_subtype(expr const & e) -> result {
     auto p     = binding_body_fresh(pred, true);
     expr body  = p.first;
     expr local = p.second;
-    format r   = bracket("{", format(local_pp_name(local)) + space() + format("\\") + space() + pp_child(body, 0).fmt(), "}");
+    format r   = bracket("{", format(local_pp_name(local)) + space() + format("//") + space() + pp_child(body, 0).fmt(), "}");
     return result(r);
 }
 
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index e0af4fb34f..489b02f744 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -87,7 +87,7 @@ void init_token_table(token_table & t) {
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type*", g_max_prec},
          {"{|", g_max_prec}, {"|}", 0}, {"(:", g_max_prec}, {":)", 0},
          {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
-         {"\\", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
+         {"//", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"abstract", g_max_prec},
          {"@@", g_max_prec}, {"@", g_max_prec},
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 9e5f63e247..4f80449cab 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -6,7 +6,7 @@ namespace lean{
 static name const * g_aliases_tk = nullptr;
 static name const * g_period_tk = nullptr;
 static name const * g_backtick_tk = nullptr;
-static name const * g_backslash_tk = nullptr;
+static name const * g_dslash_tk = nullptr;
 static name const * g_fieldarrow_tk = nullptr;
 static name const * g_placeholder_tk = nullptr;
 static name const * g_colon_tk = nullptr;
@@ -127,7 +127,7 @@ void initialize_tokens() {
     g_aliases_tk = new name{"aliases"};
     g_period_tk = new name{"."};
     g_backtick_tk = new name{"`"};
-    g_backslash_tk = new name{"\\"};
+    g_dslash_tk = new name{"//"};
     g_fieldarrow_tk = new name{"~>"};
     g_placeholder_tk = new name{"_"};
     g_colon_tk = new name{":"};
@@ -249,7 +249,7 @@ void finalize_tokens() {
     delete g_aliases_tk;
     delete g_period_tk;
     delete g_backtick_tk;
-    delete g_backslash_tk;
+    delete g_dslash_tk;
     delete g_fieldarrow_tk;
     delete g_placeholder_tk;
     delete g_colon_tk;
@@ -370,7 +370,7 @@ void finalize_tokens() {
 name const & get_aliases_tk() { return *g_aliases_tk; }
 name const & get_period_tk() { return *g_period_tk; }
 name const & get_backtick_tk() { return *g_backtick_tk; }
-name const & get_backslash_tk() { return *g_backslash_tk; }
+name const & get_dslash_tk() { return *g_dslash_tk; }
 name const & get_fieldarrow_tk() { return *g_fieldarrow_tk; }
 name const & get_placeholder_tk() { return *g_placeholder_tk; }
 name const & get_colon_tk() { return *g_colon_tk; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 983cefa24b..b135b6628e 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -8,7 +8,7 @@ void finalize_tokens();
 name const & get_aliases_tk();
 name const & get_period_tk();
 name const & get_backtick_tk();
-name const & get_backslash_tk();
+name const & get_dslash_tk();
 name const & get_fieldarrow_tk();
 name const & get_placeholder_tk();
 name const & get_colon_tk();
diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt
index 47a30ab02f..52ce24d0cc 100644
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@@ -1,7 +1,7 @@
 aliases      aliases
 period       .
 backtick     `
-backslash    \\
+dslash       //
 fieldarrow   ~>
 placeholder  _
 colon        :
diff --git a/tests/lean/curly_notation.lean b/tests/lean/curly_notation.lean
index 96a31935eb..387afd15bd 100644
--- a/tests/lean/curly_notation.lean
+++ b/tests/lean/curly_notation.lean
@@ -15,3 +15,12 @@ check { a ∈ s1 | a > 1 }
 check { a in s1 | a > 1 }
 set_option pp.unicode false
 check { a ∈ s1 | a > 2 }
+
+
+definition a := 10
+
+check ({a, a} : set nat)
+check ({a, 1, a} : set nat)
+check ({a} : set nat)
+
+check { a // a > 0 }
diff --git a/tests/lean/curly_notation.lean.expected.out b/tests/lean/curly_notation.lean.expected.out
index 6aed13c0f5..640b347733 100644
--- a/tests/lean/curly_notation.lean.expected.out
+++ b/tests/lean/curly_notation.lean.expected.out
@@ -10,3 +10,7 @@ definition s3 : set string :=
 {a ∈ s1 | a > 1} : set ℕ
 {a ∈ s1 | a > 1} : set ℕ
 {a in s1 | a > 2} : set nat
+{a, a} : set nat
+{a, 1, a} : set nat
+{a} : set nat
+{a // a > 0} : Type
diff --git a/tests/lean/print_ax1.lean.expected.out b/tests/lean/print_ax1.lean.expected.out
index 04b757a8ef..108b5ab4ae 100644
--- a/tests/lean/print_ax1.lean.expected.out
+++ b/tests/lean/print_ax1.lean.expected.out
@@ -1,3 +1,3 @@
 quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
-classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x \ Exists P → P x}
+classical.strong_indefinite_description : Π {A : Type u} (p : A → Prop), nonempty A → {x // Exists p → p x}
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
diff --git a/tests/lean/print_ax2.lean.expected.out b/tests/lean/print_ax2.lean.expected.out
index 04b757a8ef..108b5ab4ae 100644
--- a/tests/lean/print_ax2.lean.expected.out
+++ b/tests/lean/print_ax2.lean.expected.out
@@ -1,3 +1,3 @@
 quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
-classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x \ Exists P → P x}
+classical.strong_indefinite_description : Π {A : Type u} (p : A → Prop), nonempty A → {x // Exists p → p x}
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
diff --git a/tests/lean/print_ax3.lean.expected.out b/tests/lean/print_ax3.lean.expected.out
index bd14ec3c7b..30c0006fb8 100644
--- a/tests/lean/print_ax3.lean.expected.out
+++ b/tests/lean/print_ax3.lean.expected.out
@@ -1,7 +1,7 @@
 no axioms
 ------
 quot.sound : ∀ {A : Type u} [s : setoid A] {a b : A}, a ≈ b → ⟦a⟧ = ⟦b⟧
-classical.strong_indefinite_description : Π {A : Type u} (P : A → Prop), nonempty A → {x \ Exists P → P x}
+classical.strong_indefinite_description : Π {A : Type u} (p : A → Prop), nonempty A → {x // Exists p → p x}
 propext : ∀ {a b : Prop}, (a ↔ b) → a = b
 ------
 theorem foo3 : 0 = 0 :=
diff --git a/tests/lean/run/cute_binders.lean b/tests/lean/run/cute_binders.lean
index 689ede441b..5d69b23acb 100644
--- a/tests/lean/run/cute_binders.lean
+++ b/tests/lean/run/cute_binders.lean
@@ -1,9 +1,5 @@
-definition set (A : Type) := A → Prop
-definition mem {A : Type} (a : A) (s : set A) : Prop :=
-s a
 definition range (lower : nat) (upper : nat) : set nat :=
 λ a, lower ≤ a ∧ a ≤ upper
-infix ` ∈ ` := mem
 
 local notation `[` L `, ` U `]` := range L U
 
diff --git a/tests/lean/run/match2.lean b/tests/lean/run/match2.lean
index 7d9d62d40d..2d8be25158 100644
--- a/tests/lean/run/match2.lean
+++ b/tests/lean/run/match2.lean
@@ -2,6 +2,6 @@ inductive imf (f : nat → nat) : nat → Type
 | mk1 : ∀ (a : nat), imf (f a)
 | mk2 : imf (f 0 + 1)
 
-definition inv_2 (f : nat → nat) : ∀ (b : nat), imf f b → {x : nat \ x > b} →nat
+definition inv_2 (f : nat → nat) : ∀ (b : nat), imf f b → {x : nat // x > b} → nat
 | .(f a)     (imf.mk1 .f a) x := a
 | .(f 0 + 1) (imf.mk2 .f)   x := subtype.elt_of x
diff --git a/tests/lean/run/set.lean b/tests/lean/run/set.lean
deleted file mode 100644
index 56de4e71bc..0000000000
--- a/tests/lean/run/set.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-open bool nat
-
-definition set (T : Type) := T → bool
-definition mem {A : Type} (x : A) (s : set A) := s x
-infix ` ∈ ` := mem
-
-check 1 ∈ (λ x : nat, tt)
diff --git a/tests/lean/run/set2.lean b/tests/lean/run/set2.lean
deleted file mode 100644
index 7bc21a121a..0000000000
--- a/tests/lean/run/set2.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-open bool
-
-namespace set
-
-definition set (T : Type) := T → bool
-definition mem {T : Type} (a : T) (s : set T) := s a = tt
-infix `∈` := mem
-
-section
-  variable {T : Type}
-
-  definition empty : set T := λx, ff
-  notation `∅` := empty
-
-  theorem mem_empty (x : T) : ¬ (x ∈ ∅)
-  := not.intro (λH : x ∈ ∅, absurd H ff_ne_tt)
-end
-
-end set
diff --git a/tests/lean/run/sub.lean b/tests/lean/run/sub.lean
index bcb2b0539e..27c58e054d 100644
--- a/tests/lean/run/sub.lean
+++ b/tests/lean/run/sub.lean
@@ -1,3 +1,2 @@
-notation `{` binders:55 ` \ ` r:(scoped P, subtype P) `}` := r
-check { x : nat \  x > 0 }
-check { (x : nat → nat) \  true }
+check { x : nat //  x > 0 }
+check { x : nat → nat //  true }
diff --git a/tests/lean/run/sub_bug.lean b/tests/lean/run/sub_bug.lean
index d2419cd753..98a6978c1b 100644
--- a/tests/lean/run/sub_bug.lean
+++ b/tests/lean/run/sub_bug.lean
@@ -1,2 +1,2 @@
 open nat subtype
-check { x : nat \ x > 0}
+check { x : nat // x > 0}
diff --git a/tests/lean/struct_class.lean.expected.out b/tests/lean/struct_class.lean.expected.out
index 5876512a45..fd7d6c5536 100644
--- a/tests/lean/struct_class.lean.expected.out
+++ b/tests/lean/struct_class.lean.expected.out
@@ -1,6 +1,7 @@
 alternative : (Type u → Type v) → Type (max (u+1) v)
 applicative : (Type u → Type v) → Type (max (u+1) v)
 decidable : Prop → Type
+decidable_separable : Type u → (Type u → Type v) → Type (max 1 (imax (max 1 u) (max 1 u) v))
 functor : (Type u → Type v) → Type (max (u+1) v)
 has_add : Type u → Type (max 1 u)
 has_andthen : Type u → Type (max 1 u)
@@ -29,15 +30,18 @@ has_to_string : Type u → Type (max 1 u)
 has_to_tactic_format : Type → Type
 has_zero : Type u → Type (max 1 u)
 inhabited : Type u → Type (max 1 u)
+insertable : Type u → (Type u → Type v) → Type (max 1 (imax u v) v)
 is_associative : Π {A : Type u}, (A → A → A) → Type
 monad : (Type u → Type v) → Type (max (u+1) v)
 nonempty : Type u → Prop
 point : Type u_1 → Type u_2 → Type (max 1 u_1 u_2)
+separable : Type u → (Type u → Type v) → Type (max 1 (imax (max 1 u) v))
 setoid : Type u → Type (max 1 u)
 subsingleton : Type u → Prop
 alternative : (Type u → Type v) → Type (max (u+1) v)
 applicative : (Type u → Type v) → Type (max (u+1) v)
 decidable : Prop → Type
+decidable_separable : Type u → (Type u → Type v) → Type (max 1 (imax (max 1 u) (max 1 u) v))
 functor : (Type u → Type v) → Type (max (u+1) v)
 has_add : Type u → Type (max 1 u)
 has_andthen : Type u → Type (max 1 u)
@@ -66,9 +70,11 @@ has_to_string : Type u → Type (max 1 u)
 has_to_tactic_format : Type → Type
 has_zero : Type u → Type (max 1 u)
 inhabited : Type u → Type (max 1 u)
+insertable : Type u → (Type u → Type v) → Type (max 1 (imax u v) v)
 is_associative : Π {A : Type u}, (A → A → A) → Type
 monad : (Type u → Type v) → Type (max (u+1) v)
 nonempty : Type u → Prop
 point : Type u_1 → Type u_2 → Type (max 1 u_1 u_2)
+separable : Type u → (Type u → Type v) → Type (max 1 (imax (max 1 u) v))
 setoid : Type u → Type (max 1 u)
 subsingleton : Type u → Prop
diff --git a/tests/lean/subpp.lean b/tests/lean/subpp.lean
index 3f67d67df9..5f130a344d 100644
--- a/tests/lean/subpp.lean
+++ b/tests/lean/subpp.lean
@@ -1,4 +1,2 @@
 --
-open nat subtype
-
-check {x : nat \ x > 0 }
+check {x : nat // x > 0 }
diff --git a/tests/lean/subpp.lean.expected.out b/tests/lean/subpp.lean.expected.out
index 8361435712..f3614e04e1 100644
--- a/tests/lean/subpp.lean.expected.out
+++ b/tests/lean/subpp.lean.expected.out
@@ -1 +1 @@
-{x \ x > 0} : Type
+{x // x > 0} : Type