From 2ef9199c56e52c8292677411d33d5d4cfde0b3cc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 10 Nov 2020 09:53:20 -0800
Subject: [PATCH] chore: prepare to rename "predicate-like" classes

---
 src/Lean/Compiler/ConstFolding.lean | 4 ++--
 src/Lean/Delaborator.lean           | 6 +++---
 src/Lean/Elab/BuiltinNotation.lean  | 6 +++---
 src/Lean/Meta/AppBuilder.lean       | 4 ++--
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/Lean/Compiler/ConstFolding.lean b/src/Lean/Compiler/ConstFolding.lean
index f9e0623ac5..f60b246512 100644
--- a/src/Lean/Compiler/ConstFolding.lean
+++ b/src/Lean/Compiler/ConstFolding.lean
@@ -96,10 +96,10 @@ def mkNatEq (a b : Expr) : Expr :=
   mkAppN (mkConst `Eq [levelOne]) #[(mkConst `Nat), a, b]
 
 def mkNatLt (a b : Expr) : Expr :=
-  mkAppN (mkConst `Less.Less [levelZero]) #[mkConst `Nat, mkConst `Nat.less, a, b]
+  mkAppN (mkConst `HasLess.Less [levelZero]) #[mkConst `Nat, mkConst `Nat.less, a, b]
 
 def mkNatLe (a b : Expr) : Expr :=
-  mkAppN (mkConst `LessEq.LessEq [levelZero]) #[mkConst `Nat, mkConst `Nat.lessEq, a, b]
+  mkAppN (mkConst `HasLessEq.LessEq [levelZero]) #[mkConst `Nat, mkConst `Nat.lessEq, a, b]
 
 def toDecidableExpr (beforeErasure : Bool) (pred : Expr) (r : Bool) : Expr :=
   match beforeErasure, r with
diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 2033b1dda3..af292b6117 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -709,16 +709,16 @@ def delabPrefixOp (op : Bool → Syntax → Delab) : Delab := whenPPOption getPP
 @[builtinDelab app.ModN.modn] def delabModN : Delab := delabInfixOp fun _ x y => `($x %ₙ $y)
 @[builtinDelab app.Pow.pow] def delabPow : Delab := delabInfixOp fun _ x y => `($x ^ $y)
 
-@[builtinDelab app.LessEq.LessEq] def delabLE : Delab := delabInfixOp fun b x y => cond b `($x ≤ $y) `($x <= $y)
+@[builtinDelab app.HasLessEq.LessEq] def delabLE : Delab := delabInfixOp fun b x y => cond b `($x ≤ $y) `($x <= $y)
 @[builtinDelab app.GreaterEq] def delabGE : Delab := delabInfixOp fun b x y => cond b `($x ≥ $y) `($x >= $y)
-@[builtinDelab app.Less.Less] def delabLT : Delab := delabInfixOp fun _ x y => `($x < $y)
+@[builtinDelab app.HasLess.Less] def delabLT : Delab := delabInfixOp fun _ x y => `($x < $y)
 @[builtinDelab app.Greater] def delabGT : Delab := delabInfixOp fun _ x y => `($x > $y)
 @[builtinDelab app.Eq] def delabEq : Delab := delabInfixOp fun _ x y => `($x = $y)
 @[builtinDelab app.Ne] def delabNe : Delab := delabInfixOp fun _ x y => `($x ≠ $y)
 @[builtinDelab app.BEq.beq] def delabBEq : Delab := delabInfixOp fun _ x y => `($x == $y)
 @[builtinDelab app.bne] def delabBNe : Delab := delabInfixOp fun _ x y => `($x != $y)
 @[builtinDelab app.HEq] def delabHEq : Delab := delabInfixOp fun b x y => cond b `($x ≅ $y) `($x ~= $y)
-@[builtinDelab app.Equiv.Equiv] def delabEquiv : Delab := delabInfixOp fun _ x y => `($x ≈ $y)
+@[builtinDelab app.HasEquiv.Equiv] def delabEquiv : Delab := delabInfixOp fun _ x y => `($x ≈ $y)
 
 @[builtinDelab app.And] def delabAnd : Delab := delabInfixOp fun b x y => cond b `($x ∧ $y) `($x /\ $y)
 @[builtinDelab app.Or] def delabOr : Delab := delabInfixOp fun b x y => cond b `($x ∨ $y) `($x || $y)
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 289f140108..c4422a7c21 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -207,16 +207,16 @@ def expandPrefixOp (op : Name) : Macro := fun stx => do
 @[builtinMacro Lean.Parser.Term.modN] def expandModN : Macro := expandInfixOp `ModN.modn
 @[builtinMacro Lean.Parser.Term.pow] def expandPow : Macro := expandInfixOp `Pow.pow
 
-@[builtinMacro Lean.Parser.Term.le] def expandLE : Macro := expandInfixOp `LessEq.LessEq
+@[builtinMacro Lean.Parser.Term.le] def expandLE : Macro := expandInfixOp `HasLessEq.LessEq
 @[builtinMacro Lean.Parser.Term.ge] def expandGE : Macro := expandInfixOp `GreaterEq
-@[builtinMacro Lean.Parser.Term.lt] def expandLT : Macro := expandInfixOp `Less.Less
+@[builtinMacro Lean.Parser.Term.lt] def expandLT : Macro := expandInfixOp `HasLess.Less
 @[builtinMacro Lean.Parser.Term.gt] def expandGT : Macro := expandInfixOp `Greater
 @[builtinMacro Lean.Parser.Term.eq] def expandEq : Macro := expandInfixOp `Eq
 @[builtinMacro Lean.Parser.Term.ne] def expandNe : Macro := expandInfixOp `Ne
 @[builtinMacro Lean.Parser.Term.beq] def expandBEq : Macro := expandInfixOp `BEq.beq
 @[builtinMacro Lean.Parser.Term.bne] def expandBNe : Macro := expandInfixOp `bne
 @[builtinMacro Lean.Parser.Term.heq] def expandHEq : Macro := expandInfixOp `HEq
-@[builtinMacro Lean.Parser.Term.equiv] def expandEquiv : Macro := expandInfixOp `Equiv.Equiv
+@[builtinMacro Lean.Parser.Term.equiv] def expandEquiv : Macro := expandInfixOp `HasEquiv.Equiv
 
 @[builtinMacro Lean.Parser.Term.and] def expandAnd : Macro := expandInfixOp `And
 @[builtinMacro Lean.Parser.Term.or] def expandOr : Macro := expandInfixOp `Or
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index b44c2e2965..3e7ed61ee4 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -410,11 +410,11 @@ def mkDecideProof (p : Expr) : m Expr := liftMetaM do
 
 /-- Return `a < b` -/
 def mkLt (a b : Expr) : m Expr :=
-  mkAppM `Less.Less #[a, b]
+  mkAppM `HasLess.Less #[a, b]
 
 /-- Return `a <= b` -/
 def mkLe (a b : Expr) : m Expr :=
-  mkAppM `LessEq.LessEq #[a, b]
+  mkAppM `HasLessEq.LessEq #[a, b]
 
 /-- Return `arbitrary α` -/
 def mkArbitrary (α : Expr) : m Expr :=