From 1c4dea99415d36c2a5713f79d9cf02c6c2788849 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 30 Sep 2015 16:52:56 -0700
Subject: [PATCH] fix(tests/lean): adjust tests to reflect changes in the
 pretty printer

---
 tests/lean/550.lean                          |  2 +-
 tests/lean/640a.hlean                        |  6 +++---
 tests/lean/690.hlean.expected.out            |  4 ++--
 tests/lean/K_bug.lean.expected.out           |  4 ++--
 tests/lean/binder_overload.lean.expected.out |  4 ++--
 tests/lean/bug1.lean                         |  2 +-
 tests/lean/calc1.lean                        |  8 ++++----
 tests/lean/error_loc_bug.lean                |  2 +-
 tests/lean/fold.lean                         | 10 +++++-----
 tests/lean/have1.lean.expected.out           |  2 +-
 tests/lean/nary_overload.lean                |  4 ++--
 tests/lean/notation2.lean.expected.out       |  4 ++--
 tests/lean/notation3.lean                    |  2 +-
 tests/lean/notation3.lean.expected.out       |  4 ++--
 tests/lean/notation7.lean.expected.out       |  2 +-
 tests/lean/parsing_only.lean.expected.out    |  2 +-
 tests/lean/t10.lean                          |  4 ++--
 tests/lean/t10.lean.expected.out             |  6 +++---
 tests/lean/t11.lean                          |  4 ++--
 tests/lean/t14.lean                          |  2 +-
 tests/lean/t9.lean.expected.out              |  4 ++--
 21 files changed, 41 insertions(+), 41 deletions(-)

diff --git a/tests/lean/550.lean b/tests/lean/550.lean
index 27c204396..e94417d69 100644
--- a/tests/lean/550.lean
+++ b/tests/lean/550.lean
@@ -19,7 +19,7 @@ namespace bijection
     (by rewrite [compose.assoc, -{finv f ∘ _}compose.assoc, linv f, compose.left_id, linv g])
     (by rewrite [-compose.assoc, {_ ∘ finv g}compose.assoc, rinv g, compose.right_id, rinv f])
 
-  infixr `∘b`:100 := compose
+  infixr ` ∘b `:100 := compose
 
   lemma compose.assoc (f g h : bijection A) : (f ∘b g) ∘b h = f ∘b (g ∘b h) := rfl
 
diff --git a/tests/lean/640a.hlean b/tests/lean/640a.hlean
index 224a7629a..44caf6460 100644
--- a/tests/lean/640a.hlean
+++ b/tests/lean/640a.hlean
@@ -12,8 +12,8 @@ end
 section
   parameter {A : Type}
   definition relation' : A → A → Type := λa b, a = b
-  local infix `~1`:50 := relation'
-  local infix [parsing-only] `~2`:50 := relation'
+  local infix ` ~1 `:50 := relation'
+  local infix [parsing-only] ` ~2 `:50 := relation'
   variable {a : A}
   check relation' a a
   check a ~1 a
@@ -23,7 +23,7 @@ end
 section
   parameter {A : Type}
   definition relation'' : A → A → Type := λa b, a = b
-  local infix [parsing-only] `~2`:50 := relation''
+  local infix [parsing-only] ` ~2 `:50 := relation''
   variable {a : A}
   check relation'' a a
   check a ~2 a
diff --git a/tests/lean/690.hlean.expected.out b/tests/lean/690.hlean.expected.out
index 4d05275fd..603fce6f0 100644
--- a/tests/lean/690.hlean.expected.out
+++ b/tests/lean/690.hlean.expected.out
@@ -7,14 +7,14 @@ u₂ : B u₁,
 v₁ : A,
 v₂ : B v₁,
 p : ⟨u₁, u₂⟩.1 = ⟨v₁, v₂⟩.1,
-q : u₂ =[ p ] v₂
+q : u₂ =[p] v₂
 ⊢ ⟨(sigma_eq p q)..1, (sigma_eq p q)..2⟩ = ⟨p, q⟩
 690.hlean:12:0: error: don't know how to synthesize placeholder
 A : Type,
 B : A → Type,
 u v : Σ (a : A), B a,
 p : u.1 = v.1,
-q : u.2 =[ p ] v.2
+q : u.2 =[p] v.2
 ⊢ ⟨(sigma_eq p q)..1, (sigma_eq p q)..2⟩ = ⟨p, q⟩
 690.hlean:12:0: error: failed to add declaration 'dpair_sigma_eq' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
diff --git a/tests/lean/K_bug.lean.expected.out b/tests/lean/K_bug.lean.expected.out
index fdb434fbc..acf7bb0cf 100644
--- a/tests/lean/K_bug.lean.expected.out
+++ b/tests/lean/K_bug.lean.expected.out
@@ -1,6 +1,6 @@
 K_bug.lean:14:24: error: type mismatch at term
-  pred_succ n ⁻¹
+  pred_succ n⁻¹
 has type
-  pred (succ n ⁻¹) = n ⁻¹
+  pred (succ n⁻¹) = n⁻¹
 but is expected to have type
   n = pred (succ n)
diff --git a/tests/lean/binder_overload.lean.expected.out b/tests/lean/binder_overload.lean.expected.out
index 743b02443..4bfac196e 100644
--- a/tests/lean/binder_overload.lean.expected.out
+++ b/tests/lean/binder_overload.lean.expected.out
@@ -1,5 +1,5 @@
-{x : ℕ ∈ S| x > 0} : set ℕ
-{x : ℕ ∈ s| x > 0} : finset ℕ
+{x : ℕ ∈ S | x > 0} : set ℕ
+{x : ℕ ∈ s | x > 0} : finset ℕ
 @set.sep.{1} nat (λ (x : nat), nat.gt x (nat.of_num 0)) S : set.{1} nat
 @finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b) (λ (x : nat), nat.gt x (nat.of_num 0))
   (λ (a : nat), nat.decidable_ge a (nat.succ (nat.of_num 0)))
diff --git a/tests/lean/bug1.lean b/tests/lean/bug1.lean
index 7bdbf1364..a5d572fe5 100644
--- a/tests/lean/bug1.lean
+++ b/tests/lean/bug1.lean
@@ -1,6 +1,6 @@
 prelude definition bool  : Type.{1}           := Type.{0}
 definition and   (p q : bool) : bool  := ∀ c : bool, (p → q → c) → c
-infixl `∧`:25 := and
+infixl ` ∧ `:25 := and
 
 constant a : bool
 
diff --git a/tests/lean/calc1.lean b/tests/lean/calc1.lean
index 521e440f1..ba8eb878e 100644
--- a/tests/lean/calc1.lean
+++ b/tests/lean/calc1.lean
@@ -1,12 +1,12 @@
 prelude constant A : Type.{1}
 definition bool : Type.{1} := Type.{0}
 constant eq : A → A → bool
-infixl `=`:50 := eq
+infixl ` = `:50 := eq
 axiom subst (P : A → bool) (a b : A) (H1 : a = b) (H2 : P a) : P b
 axiom eq_trans (a b c : A) (H1 : a = b) (H2 : b = c) : a = c
 axiom eq_refl (a : A) : a = a
 constant le : A → A → bool
-infixl `≤`:50 := le
+infixl ` ≤ `:50 := le
 axiom le_trans (a b c : A) (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c
 axiom le_refl (a : A) : a ≤ a
 axiom eq_le_trans (a b c : A) (H1 : a = b) (H2 : b ≤ c) : a ≤ c
@@ -29,7 +29,7 @@ check calc a   = b : H1
            ... = e : H4
 
 constant lt : A → A → bool
-infixl `<`:50 := lt
+infixl ` < `:50 := lt
 axiom lt_trans (a b c : A) (H1 : a < b) (H2 : b < c) : a < c
 axiom le_lt_trans (a b c : A) (H1 : a ≤ b) (H2 : b < c) : a < c
 axiom lt_le_trans (a b c : A) (H1 : a < b) (H2 : b ≤ c) : a < c
@@ -41,7 +41,7 @@ check calc b  ≤ c : H2
           ... < d : H5
 
 constant le2 : A → A → bool
-infixl `≤`:50 := le2
+infixl ` ≤ `:50 := le2
 constant le2_trans (a b c : A) (H1 : le2 a b) (H2 : le2 b c) : le2 a c
 attribute le2_trans [trans]
 print raw calc b   ≤ c : H2
diff --git a/tests/lean/error_loc_bug.lean b/tests/lean/error_loc_bug.lean
index 2aa700277..ea7734438 100644
--- a/tests/lean/error_loc_bug.lean
+++ b/tests/lean/error_loc_bug.lean
@@ -39,7 +39,7 @@ namespace PropF
 
   definition valuation   := PropVar → bool
 
-  reserve infix `⊢`:26
+  reserve infix ` ⊢ `:26
 
   /- Provability -/
 
diff --git a/tests/lean/fold.lean b/tests/lean/fold.lean
index 4d88f2ea8..8f83d0a48 100644
--- a/tests/lean/fold.lean
+++ b/tests/lean/fold.lean
@@ -1,17 +1,17 @@
 prelude
 definition Prop := Type.{0} inductive true : Prop := intro : true inductive false : Prop constant num : Type
-inductive prod (A B : Type) := mk : A → B → prod A B infixl `×`:30 := prod
+inductive prod (A B : Type) := mk : A → B → prod A B infixl ` × `:30 := prod
 variables a b c : num
 
 section
-  local notation `(` t:(foldr `,` (e r, prod.mk e r)) `)` := t
+  local notation `(` t:(foldr `, ` (e r, prod.mk e r)) `)` := t
   check (a, false, b, true, c)
   set_option pp.notation false
   check (a, false, b, true, c)
 end
 
 section
-  local notation `(` t:(foldr `,` (e r, prod.mk r e)) `)` := t
+  local notation `(` t:(foldr `, ` (e r, prod.mk r e)) `)` := t
   set_option pp.notation true
   check (a, false, b, true, c)
   set_option pp.notation false
@@ -19,7 +19,7 @@ section
 end
 
 section
-  local notation `(` t:(foldl `,` (e r, prod.mk r e)) `)` := t
+  local notation `(` t:(foldl `, ` (e r, prod.mk r e)) `)` := t
   set_option pp.notation true
   check (a, false, b, true, c)
   set_option pp.notation false
@@ -27,7 +27,7 @@ section
 end
 
 section
-  local notation `(` t:(foldl `,` (e r, prod.mk e r)) `)` := t
+  local notation `(` t:(foldl `, ` (e r, prod.mk e r)) `)` := t
   set_option pp.notation true
   check (a, false, b, true, c)
   set_option pp.notation false
diff --git a/tests/lean/have1.lean.expected.out b/tests/lean/have1.lean.expected.out
index 4e5be8d79..2f644230f 100644
--- a/tests/lean/have1.lean.expected.out
+++ b/tests/lean/have1.lean.expected.out
@@ -3,6 +3,6 @@ have e2 : a = c, from e1 ⬝ H2,
 have e3 : c = a, from e2⁻¹,
 assert e4 : b = a, from e1⁻¹,
 have e5 : b = c, from e4 ⬝ e2,
-have e6 : a = a, from H1 ⬝ H2 ⬝ H2 ⁻¹ ⬝ H1 ⁻¹ ⬝ H1 ⬝ H2 ⬝ H2 ⁻¹ ⬝ H1 ⁻¹,
+have e6 : a = a, from H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹ ⬝ H1 ⬝ H2 ⬝ H2⁻¹ ⬝ H1⁻¹,
 e3 ⬝ e2 :
   c = c
diff --git a/tests/lean/nary_overload.lean b/tests/lean/nary_overload.lean
index 97fe35e85..d047d85c8 100644
--- a/tests/lean/nary_overload.lean
+++ b/tests/lean/nary_overload.lean
@@ -7,8 +7,8 @@ constant lst.nil {A : Type} : lst A
 constant vec.cons {A : Type} : A → vec A → vec A
 constant lst.cons {A : Type} : A → lst A → lst A
 
-notation `[` l:(foldr `,` (h t, vec.cons h t) vec.nil `]`) := l
-notation `[` l:(foldr `,` (h t, lst.cons h t) lst.nil `]`) := l
+notation `[` l:(foldr `, ` (h t, vec.cons h t) vec.nil `]`) := l
+notation `[` l:(foldr `, ` (h t, lst.cons h t) lst.nil `]`) := l
 
 constant A : Type.{1}
 variables a b c : A
diff --git a/tests/lean/notation2.lean.expected.out b/tests/lean/notation2.lean.expected.out
index d2f39b631..18ed447eb 100644
--- a/tests/lean/notation2.lean.expected.out
+++ b/tests/lean/notation2.lean.expected.out
@@ -1,2 +1,2 @@
-1 :: 2 :: nil : list num
-1 :: 2 :: 3 :: 4 :: 5 :: nil : list num
+1::2::nil : list num
+1::2::3::4::5::nil : list num
diff --git a/tests/lean/notation3.lean b/tests/lean/notation3.lean
index 65def3ce7..6452742a9 100644
--- a/tests/lean/notation3.lean
+++ b/tests/lean/notation3.lean
@@ -1,5 +1,5 @@
 import data.prod data.num
-inductive list (T : Type) : Type := nil {} : list T | cons   : T → list T → list T open list notation h :: t  := cons h t notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
+inductive list (T : Type) : Type := nil {} : list T | cons   : T → list T → list T open list notation h :: t  := cons h t notation `[` l:(foldr `, ` (h t, cons h t) nil) `]` := l
 open prod num
 constants a b : num
 check [a, b, b]
diff --git a/tests/lean/notation3.lean.expected.out b/tests/lean/notation3.lean.expected.out
index 66caff64b..80fbf04aa 100644
--- a/tests/lean/notation3.lean.expected.out
+++ b/tests/lean/notation3.lean.expected.out
@@ -1,4 +1,4 @@
-[ a, b, b ] : list num
+[a, b, b] : list num
 (a, true, a = b, b) : num × Prop × Prop × num
 (a, b) : num × num
-[ 1, 2 + 2, 3 ] : list num
+[1, 2 + 2, 3] : list num
diff --git a/tests/lean/notation7.lean.expected.out b/tests/lean/notation7.lean.expected.out
index 42830822c..1e7601c26 100644
--- a/tests/lean/notation7.lean.expected.out
+++ b/tests/lean/notation7.lean.expected.out
@@ -1,2 +1,2 @@
-g 0 :+1 :+1 (1 :+1 + 2 :+1) :+1 : num
+g 0:+1:+1 (1:+1 + 2:+1):+1 : num
 g (f (f 0)) (f (add (f 1) (f 2))) : num
diff --git a/tests/lean/parsing_only.lean.expected.out b/tests/lean/parsing_only.lean.expected.out
index 2df76179f..825a48b2a 100644
--- a/tests/lean/parsing_only.lean.expected.out
+++ b/tests/lean/parsing_only.lean.expected.out
@@ -1,3 +1,3 @@
-10 +++ : num
+10+++ : num
 g 10 : num
 Type : Type
diff --git a/tests/lean/t10.lean b/tests/lean/t10.lean
index 14021dc72..274b28fc0 100644
--- a/tests/lean/t10.lean
+++ b/tests/lean/t10.lean
@@ -8,7 +8,7 @@ constant q : B
 constant x : N
 constant y : N
 constant z : N
-infixr `∧`:25 := and
+infixr ` ∧ `:25 := and
 notation `if` c `then` t:45 `else` e:45 := ite c t e
 check if p ∧ q then f x else y
 check if p ∧ q then q else y
@@ -16,7 +16,7 @@ constant list : Type.{1}
 constant nil : list
 constant cons : N → list → list
 -- Non empty lists
-notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
+notation `[` l:(foldr `, ` (h t, cons h t) nil) `]` := l
 check [x, y, z, x, y, y]
 check [x]
 notation `[` `]` := nil
diff --git a/tests/lean/t10.lean.expected.out b/tests/lean/t10.lean.expected.out
index c32b625e6..d15961abd 100644
--- a/tests/lean/t10.lean.expected.out
+++ b/tests/lean/t10.lean.expected.out
@@ -7,6 +7,6 @@ has type
   B
 but is expected to have type
   N
-[ x, y, z, x, y, y ] : list
-[ x ] : list
-[ ] : list
+[x, y, z, x, y, y] : list
+[x] : list
+[] : list
diff --git a/tests/lean/t11.lean b/tests/lean/t11.lean
index 104807a34..f0e5ef7cf 100644
--- a/tests/lean/t11.lean
+++ b/tests/lean/t11.lean
@@ -1,8 +1,8 @@
 prelude constant A    : Type.{1}
 definition bool : Type.{1} := Type.{0}
 constant Exists (P : A → bool) : bool
-notation `exists` binders `,` b:(scoped b, Exists b) := b
-notation `∃` binders `,` b:(scoped b, Exists b) := b
+notation `exists` binders `, ` b:(scoped b, Exists b) := b
+notation `∃` binders `, ` b:(scoped b, Exists b) := b
 constant p : A → bool
 constant q : A → A → bool
 check exists x : A, p x
diff --git a/tests/lean/t14.lean b/tests/lean/t14.lean
index 448448b2c..145482b3d 100644
--- a/tests/lean/t14.lean
+++ b/tests/lean/t14.lean
@@ -32,7 +32,7 @@ end
 
 namespace foo
   constant f : A → A → A
-  infix `*`:75 := f
+  infix ` * `:75 := f
 end foo
 
 section
diff --git a/tests/lean/t9.lean.expected.out b/tests/lean/t9.lean.expected.out
index 82c3ec2fb..211aaa792 100644
--- a/tests/lean/t9.lean.expected.out
+++ b/tests/lean/t9.lean.expected.out
@@ -1,3 +1,3 @@
-a + b * a : N
+a+b*a : N
 t9.lean:16:7: error: invalid expression
-a + b * a : N
+a+b*a : N