From 964fd3f520bfacace8f74726f83cd8cf81f78ce9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Apr 2021 20:22:43 -0700
Subject: [PATCH] chore: fixes tests

closes #405
---
 tests/lean/implicitLambdaIssue.lean     |  6 +++---
 tests/lean/macroStack.lean.expected.out |  2 +-
 tests/lean/run/binrel.lean              | 20 ++++++++++----------
 tests/lean/run/implicitApplyIssue.lean  |  2 +-
 tests/lean/run/inductive1.lean          |  4 +---
 tests/lean/run/inductive_pred.lean      |  2 ++
 tests/lean/run/monotone.lean            |  4 ++--
 tests/lean/run/noindexAnnotation.lean   |  2 +-
 tests/lean/uintCtors.lean               |  4 ++--
 9 files changed, 23 insertions(+), 23 deletions(-)

diff --git a/tests/lean/implicitLambdaIssue.lean b/tests/lean/implicitLambdaIssue.lean
index 784dd9f7c3..b789cd744b 100644
--- a/tests/lean/implicitLambdaIssue.lean
+++ b/tests/lean/implicitLambdaIssue.lean
@@ -1,12 +1,12 @@
 class HasMem (α : outParam $ Type u) (β : Type v) where
     mem : α → β → Prop
 
-class PartialOrder (P : Type u) extends HasLessEq P where
+class PartialOrder (P : Type u) extends LE P where
   refl (s : P) : s ≤ s
   antisymm (s t : P) : s ≤ t → t ≤ s → s = t
   trans (s t u : P) : s ≤ t → t ≤ u → s ≤ u
 
-theorem HasLessEq.LessEq.trans {P : Type _} [PartialOrder P] {x y z : P} : x ≤ y → y ≤ z → x ≤ z := PartialOrder.trans _ _ _
+theorem LE.le.trans {P : Type _} [PartialOrder P] {x y z : P} : x ≤ y → y ≤ z → x ≤ z := PartialOrder.trans _ _ _
 
 infix:50 " ∈ " => HasMem.mem
 
@@ -19,7 +19,7 @@ instance : HasMem α (Set α) := ⟨λ a s => s a⟩
 theorem ext {s t : Set α} (h : ∀ x, x ∈ s ↔ x ∈ t) : s = t :=
   funext $ λ x => propext $ h x
 
-instance : HasLessEq (Set α) := ⟨λ s t => ∀ {x : α}, x ∈ s → x ∈ t⟩
+instance : LE (Set α) := ⟨λ s t => ∀ {x : α}, x ∈ s → x ∈ t⟩
 
 instance : PartialOrder (Set α) where
   refl := λ s x => id
diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out
index 610e9e8141..00fe9c6647 100644
--- a/tests/lean/macroStack.lean.expected.out
+++ b/tests/lean/macroStack.lean.expected.out
@@ -1,7 +1,7 @@
 macroStack.lean:4:5-4:6: error: unknown identifier 'x'
 macroStack.lean:8:6-8:7: error: unknown identifier 'x'
 with resulting expansion
-  binrel% Greater✝ x 0
+  binrel% GT.gt✝ x 0
 while expanding
   x > 0
 while expanding
diff --git a/tests/lean/run/binrel.lean b/tests/lean/run/binrel.lean
index e7bceba7af..78459c1354 100644
--- a/tests/lean/run/binrel.lean
+++ b/tests/lean/run/binrel.lean
@@ -1,35 +1,35 @@
 def ex1 (x y : Nat) (i j : Int) :=
-  binrel% Less x i
+  binrel% LT.lt x i
 
 def ex2 (x y : Nat) (i j : Int) :=
-  binrel% Less i x
+  binrel% LT.lt i x
 
 def ex3 (x y : Nat) (i j : Int) :=
-  binrel% Less (i + 1) x
+  binrel% LT.lt (i + 1) x
 
 def ex4 (x y : Nat) (i j : Int) :=
-  binrel% Less i (x + 1)
+  binrel% LT.lt i (x + 1)
 
 def ex5 (x y : Nat) (i j : Int) :=
-  binrel% Less i (x + y)
+  binrel% LT.lt i (x + y)
 
 def ex6 (x y : Nat) (i j : Int) :=
-  binrel% Less (i + j) (x + 0)
+  binrel% LT.lt (i + j) (x + 0)
 
 def ex7 (x y : Nat) (i j : Int) :=
-  binrel% Less (i + j) (x + i)
+  binrel% LT.lt (i + j) (x + i)
 
 def ex8 (x y : Nat) (i j : Int) :=
-  binrel% Less (i + 0) (x + i)
+  binrel% LT.lt (i + 0) (x + i)
 
 def ex9 (n : UInt32) :=
-  binrel% Less n 0xd800
+  binrel% LT.lt n 0xd800
 
 def ex10 (x : Lean.Syntax) : Bool :=
   x.getArgs.all (binrel% BEq.beq ·.getKind `foo)
 
 def ex11 (xs : Array (Nat × Nat)) :=
-  let f a b := binrel% Less a.1 b.1
+  let f a b := binrel% LT.lt a.1 b.1
   f xs[1] xs[2]
 
 def ex12 (i j : Int) :=
diff --git a/tests/lean/run/implicitApplyIssue.lean b/tests/lean/run/implicitApplyIssue.lean
index aaf772b550..77bf5b34cd 100644
--- a/tests/lean/run/implicitApplyIssue.lean
+++ b/tests/lean/run/implicitApplyIssue.lean
@@ -7,7 +7,7 @@ infix:50 " ∈ " => HasMem.mem
 
 instance : HasMem α (Set α) := ⟨λ a s => s a⟩
 
-instance : HasLessEq (Set α) := ⟨λ s t => ∀ {x : α}, x ∈ s → x ∈ t⟩
+instance : LE (Set α) := ⟨λ s t => ∀ {x : α}, x ∈ s → x ∈ t⟩
 
 class HasInf (P : Type u) where
   inf : P → P → P
diff --git a/tests/lean/run/inductive1.lean b/tests/lean/run/inductive1.lean
index ed52ba27f8..8b6dbcf8ba 100644
--- a/tests/lean/run/inductive1.lean
+++ b/tests/lean/run/inductive1.lean
@@ -1,5 +1,3 @@
-
-
 inductive L1.{u} (α : Type u)
 | nil
 | cons : α → L1 α → L1 α
@@ -80,7 +78,7 @@ inductive ListLast {α : Type u} : List α → Type u
 inductive Test : Nat → Type
 | mk : Test ((fun n => n.succ) Nat.zero)
 
-inductive SortedMap {α : Type u} {β : Type v} [HasLess α] : List (α × β) → Prop
+inductive SortedMap {α : Type u} {β : Type v} [LT α] : List (α × β) → Prop
 | nil : SortedMap []
 | cons : ∀ (k : α) (v : β) (l : List (α × β)),
          SortedMap l →
diff --git a/tests/lean/run/inductive_pred.lean b/tests/lean/run/inductive_pred.lean
index 4928af43c4..286c4dce9c 100644
--- a/tests/lean/run/inductive_pred.lean
+++ b/tests/lean/run/inductive_pred.lean
@@ -1,3 +1,4 @@
+namespace Ex
 inductive LE : Nat → Nat → Prop
   | refl : LE n n
   | succ : LE n m → LE n m.succ
@@ -44,3 +45,4 @@ theorem Power2.mul : Power2 n → Power2 m → Power2 (n*m) := by
 -- theorem Power2.mul' : Power2 n → Power2 m → Power2 (n*m)
 --  | h1, base => by simp_all
 --  | h1, ind h2 => mul_left_comm .. ▸ ind (mul' h1 h2)
+end Ex
diff --git a/tests/lean/run/monotone.lean b/tests/lean/run/monotone.lean
index f861ca81b1..0939b142af 100644
--- a/tests/lean/run/monotone.lean
+++ b/tests/lean/run/monotone.lean
@@ -1,9 +1,9 @@
-class Preorder (α : Type u) extends HasLessEq α where
+class Preorder (α : Type u) extends LE α where
   le_refl  (a : α) : a ≤ a
   le_trans {a b c : α} : a ≤ b → b ≤ c → a ≤ c
 
 instance {α : Type u} {β : α → Type v} [(a : α) → Preorder (β a)] : Preorder ((a : α) → β a) where
-  LessEq f g := ∀ a, f a ≤ g a
+  le f g := ∀ a, f a ≤ g a
   le_refl f  := fun a => Preorder.le_refl (f a)
   le_trans   := fun h₁ h₂ a => Preorder.le_trans (h₁ a) (h₂ a)
 
diff --git a/tests/lean/run/noindexAnnotation.lean b/tests/lean/run/noindexAnnotation.lean
index d8b4692ea0..17a5632827 100644
--- a/tests/lean/run/noindexAnnotation.lean
+++ b/tests/lean/run/noindexAnnotation.lean
@@ -1,6 +1,6 @@
 structure Fin2 (n : Nat) :=
   (val  : Nat)
-  (isLt : Less val n)
+  (isLt : val < n)
 
 protected def Fin2.ofNat {n : Nat} (a : Nat) : Fin2 (Nat.succ n) :=
   ⟨a % Nat.succ n, Nat.mod_lt _ (Nat.zeroLtSucc _)⟩
diff --git a/tests/lean/uintCtors.lean b/tests/lean/uintCtors.lean
index 60354218c8..b19594c36a 100644
--- a/tests/lean/uintCtors.lean
+++ b/tests/lean/uintCtors.lean
@@ -1,10 +1,10 @@
-def UInt32.ofNatCore' (n : Nat) (h : Less n UInt32.size) : UInt32 := {
+def UInt32.ofNatCore' (n : Nat) (h : n < UInt32.size) : UInt32 := {
   val := { val := n, isLt := h }
 }
 
 #eval UInt32.ofNatCore' 10 (by decide)
 
-def UInt64.ofNatCore' (n : Nat) (h : Less n UInt64.size) : UInt64 := {
+def UInt64.ofNatCore' (n : Nat) (h : n < UInt64.size) : UInt64 := {
   val := { val := n, isLt := h }
 }