diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean
index 6d3a6b414c..3d0502c4ba 100644
--- a/src/Init/Data/Ord.lean
+++ b/src/Init/Data/Ord.lean
@@ -10,7 +10,7 @@ import Init.Data.String
 
 inductive Ordering where
   | lt | eq | gt
-deriving Inhabited
+deriving Inhabited, BEq
 
 
 class Ord (α : Type u) where
@@ -37,3 +37,14 @@ instance : Ord Bool where
 
 instance : Ord String where
   compare x y := compareOfLessAndEq x y
+
+instance (n : Nat) : Ord (Fin n) where
+  compare x y := compare x.val y.val
+
+def USize.cmp (a b : USize) : Ordering := compare a.val b.val
+
+instance : Ord USize where
+  compare x y := compare x.val y.val
+
+instance : Ord Char where 
+  compare x y := compareOfLessAndEq x y
\ No newline at end of file
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 22b2fd5bf9..2d32b29d51 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -830,7 +830,7 @@ instance : LT UInt32 where
 
 instance : LE UInt32 where
   le a b := LE.le a.val b.val
-
+ 
 set_option bootstrap.genMatcherCode false in
 @[extern c inline "#1 < #2"]
 def UInt32.decLt (a b : UInt32) : Decidable (LT.lt a b) :=
diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean
index 542d52bbc7..8931dcb121 100644
--- a/src/Lean/Compiler/IR/Basic.lean
+++ b/src/Lean/Compiler/IR/Basic.lean
@@ -440,7 +440,7 @@ end Decl
 open Std (RBTree RBTree.empty RBMap)
 
 /-- Set of variable and join point names -/
-abbrev IndexSet := RBTree Index Index.lt
+abbrev IndexSet := RBTree Index compare
 instance : Inhabited IndexSet := ⟨{}⟩
 
 def mkIndexSet (idx : Index) : IndexSet :=
@@ -451,7 +451,7 @@ inductive LocalContextEntry where
   | localVar  : IRType → Expr → LocalContextEntry
   | joinPoint : Array Param → FnBody → LocalContextEntry
 
-abbrev LocalContext := RBMap Index LocalContextEntry Index.lt
+abbrev LocalContext := RBMap Index LocalContextEntry compare
 
 def LocalContext.addLocal (ctx : LocalContext) (x : VarId) (t : IRType) (v : Expr) : LocalContext :=
   ctx.insert x.idx (LocalContextEntry.localVar t v)
@@ -507,7 +507,7 @@ def LocalContext.getValue (ctx : LocalContext) (x : VarId) : Option Expr :=
   | some (LocalContextEntry.localVar _ v) => some v
   | other => none
 
-abbrev IndexRenaming := RBMap Index Index Index.lt
+abbrev IndexRenaming := RBMap Index Index compare
 
 class AlphaEqv (α : Type) where
   aeqv : IndexRenaming → α → α → Bool
@@ -599,7 +599,7 @@ def FnBody.beq (b₁ b₂ : FnBody) : Bool :=
 
 instance : BEq FnBody := ⟨FnBody.beq⟩
 
-abbrev VarIdSet := RBTree VarId (fun x y => x.idx < y.idx)
+abbrev VarIdSet := RBTree VarId (fun x y => compare x.idx y.idx)
 instance : Inhabited VarIdSet := ⟨{}⟩
 
 def mkIf (x : VarId) (t e : FnBody) : FnBody :=
diff --git a/src/Lean/Compiler/IR/LiveVars.lean b/src/Lean/Compiler/IR/LiveVars.lean
index f93de87be4..1ef00ff116 100644
--- a/src/Lean/Compiler/IR/LiveVars.lean
+++ b/src/Lean/Compiler/IR/LiveVars.lean
@@ -79,7 +79,7 @@ def FnBody.hasLiveVar (b : FnBody) (ctx : LocalContext) (x : VarId) : Bool :=
   (IsLive.visitFnBody x.idx b).run' ctx
 
 abbrev LiveVarSet   := VarIdSet
-abbrev JPLiveVarMap := Std.RBMap JoinPointId LiveVarSet (fun j₁ j₂ => j₁.idx < j₂.idx)
+abbrev JPLiveVarMap := Std.RBMap JoinPointId LiveVarSet (fun j₁ j₂ => compare j₁.idx j₂.idx)
 
 instance : Inhabited LiveVarSet where
   default := {}
diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean
index 4130cf2c73..a715be72d5 100644
--- a/src/Lean/Compiler/IR/RC.lean
+++ b/src/Lean/Compiler/IR/RC.lean
@@ -19,7 +19,7 @@ structure VarInfo where
   consume    : Bool := false -- true if the variable RC must be "consumed"
   deriving Inhabited
 
-abbrev VarMap := Std.RBMap VarId VarInfo (fun x y => x.idx < y.idx)
+abbrev VarMap := Std.RBMap VarId VarInfo (fun x y => compare x.idx y.idx)
 
 structure Context where
   env            : Environment
diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean
index 3df3c6d74b..bac04fa99e 100644
--- a/src/Lean/Data/Json/Basic.lean
+++ b/src/Lean/Data/Json/Basic.lean
@@ -45,6 +45,7 @@ protected def normalize : JsonNumber → Int × Nat × Int
           break
       (sign, mAbs, -(e : Int) + nDigits)
 
+-- todo (Dany): We should have an Ordering version of this.
 def lt (a b : JsonNumber) : Bool :=
   let (as, am, ae) := a.normalize
   let (bs, bm, be) := b.normalize
@@ -77,6 +78,12 @@ instance : LT JsonNumber :=
 
 instance (a b : JsonNumber) : Decidable (a < b) :=
   inferInstanceAs (Decidable (lt a b = true))
+  
+instance : Ord JsonNumber where
+  compare x y := 
+    if x < y then Ordering.lt 
+    else if x > y then Ordering.gt
+    else Ordering.eq
 
 protected def toString : JsonNumber → String
   | ⟨m, 0⟩ => m.repr
@@ -140,7 +147,7 @@ def mkObj (o : List (String × Json)) : Json :=
   obj $ do
     let mut kvPairs := RBNode.leaf
     for ⟨k, v⟩ in o do
-      kvPairs := kvPairs.insert strLt k v
+      kvPairs := kvPairs.insert compare k v
     kvPairs
 
 instance : Coe Nat Json := ⟨fun n => Json.num n⟩
@@ -181,7 +188,7 @@ def getNum? : Json → Option JsonNumber
   | _     => none
 
 def getObjVal? : Json → String → Option Json
-  | obj kvs, k => kvs.find strLt k
+  | obj kvs, k => kvs.find compare k
   | _      , _ => none
 
 def getArrVal? : Json → Nat → Option Json
@@ -192,7 +199,7 @@ def getObjValD (j : Json) (k : String) : Json :=
   (j.getObjVal? k).getD null
 
 def setObjVal! : Json → String → Json → Json
-  | obj kvs, k, v => obj <| kvs.insert strLt k v
+  | obj kvs, k, v => obj <| kvs.insert compare k v
   | j      , _, _ => panic! "Json.setObjVal!: not an object: {j}"
 
 inductive Structured where
diff --git a/src/Lean/Data/Json/Parser.lean b/src/Lean/Data/Json/Parser.lean
index a243aaa8bb..c3d8b434fc 100644
--- a/src/Lean/Data/Json/Parser.lean
+++ b/src/Lean/Data/Json/Parser.lean
@@ -249,7 +249,7 @@ partial def objectCore (anyCore : Unit → Quickparse Json) : Quickparse (RBNode
   else if c = ',' then
     ws
     let kvs ← objectCore anyCore
-    kvs.insert strLt k v
+    kvs.insert compare k v
   else
     fail "unexpected character in object"
 
diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean
index 9ab50c5c55..811e10add4 100644
--- a/src/Lean/Data/JsonRpc.lean
+++ b/src/Lean/Data/JsonRpc.lean
@@ -21,7 +21,7 @@ inductive RequestID where
   | str (s : String)
   | num (n : JsonNumber)
   | null
-  deriving Inhabited, BEq
+  deriving Inhabited, BEq, Ord
 
 instance : ToString RequestID where
   toString
diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index e1248607b7..4f80d525bc 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -65,26 +65,46 @@ def isSuffixOf : Name → Name → Bool
   | num p₁ n₁ _, num p₂ n₂ _ => n₁ == n₂ && isSuffixOf p₁ p₂
   | _,           _           => false
 
-def lt : Name → Name → Bool
-  | anonymous,   anonymous   => false
-  | anonymous,   _           => true
-  | num p₁ i₁ _, num p₂ i₂ _ => lt p₁ p₂ || (p₁ == p₂ && i₁ < i₂)
-  | num _ _ _,   str _ _ _   => true
-  | str p₁ n₁ _, str p₂ n₂ _ => lt p₁ p₂ || (p₁ == p₂ && n₁ < n₂)
-  | _,           _           => false
+def cmp : Name → Name → Ordering
+  | anonymous,   anonymous   => Ordering.eq
+  | anonymous,   _           => Ordering.lt
+  | _,           anonymous   => Ordering.gt
+  | num p₁ i₁ _, num p₂ i₂ _ => 
+    match cmp p₁ p₂ with  
+    | Ordering.eq => compare i₁ i₂
+    | ord => ord
+  | num _ _ _,   str _ _ _   => Ordering.lt
+  | str _ _ _,   num _ _ _   => Ordering.gt
+  | str p₁ n₁ _, str p₂ n₂ _ => 
+    match cmp p₁ p₂ with 
+    | Ordering.eq => compare n₁ n₂
+    | ord => ord
+    
+def lt (x y : Name) : Bool :=
+  cmp x y == Ordering.lt
 
-def quickLtAux : Name → Name → Bool
-  | anonymous, anonymous   => false
-  | anonymous, _           => true
-  | num n v _, num n' v' _ => v < v' || (v = v' && n.quickLtAux n')
-  | num _ _ _, str _ _ _   => true
-  | str n s _, str n' s' _ => s < s' || (s = s' && n.quickLtAux n')
-  | _,         _           => false
+def quickCmpAux : Name → Name → Ordering 
+  | anonymous, anonymous   => Ordering.eq
+  | anonymous, _           => Ordering.lt
+  | _,         anonymous   => Ordering.gt
+  | num n v _, num n' v' _ => 
+    match compare v v' with
+    | Ordering.eq => n.quickCmpAux n'
+    | ord => ord
+  | num _ _ _, str _ _ _   => Ordering.lt
+  | str _ _ _, num _ _ _   => Ordering.gt
+  | str n s _, str n' s' _ => 
+    match compare s s' with
+    | Ordering.eq => n.quickCmpAux n'
+    | ord => ord
+
+def quickCmp (n₁ n₂ : Name) : Ordering :=
+  match compare n₁.hash n₂.hash with
+  | Ordering.eq => quickCmpAux n₁ n₂
+  | ord => ord
 
 def quickLt (n₁ n₂ : Name) : Bool :=
-  if n₁.hash < n₂.hash then true
-  else if n₁.hash > n₂.hash then false
-  else quickLtAux n₁ n₂
+  quickCmp n₁ n₂ == Ordering.lt
 
 /- Alternative HasLt instance. -/
 @[inline] protected def hasLtQuick : LT Name :=
@@ -122,9 +142,9 @@ end Name
 
 open Std (RBMap RBTree mkRBMap mkRBTree)
 
-def NameMap (α : Type) := Std.RBMap Name α Name.quickLt
+def NameMap (α : Type) := Std.RBMap Name α Name.quickCmp
 
-@[inline] def mkNameMap (α : Type) : NameMap α := Std.mkRBMap Name α Name.quickLt
+@[inline] def mkNameMap (α : Type) : NameMap α := Std.mkRBMap Name α Name.quickCmp
 
 namespace NameMap
 variable {α : Type}
@@ -142,10 +162,10 @@ def contains (m : NameMap α) (n : Name) : Bool := Std.RBMap.contains m n
 
 end NameMap
 
-def NameSet := RBTree Name Name.quickLt
+def NameSet := RBTree Name Name.quickCmp
 
 namespace NameSet
-def empty : NameSet := mkRBTree Name Name.quickLt
+def empty : NameSet := mkRBTree Name Name.quickCmp
 instance : EmptyCollection NameSet := ⟨empty⟩
 instance : Inhabited NameSet := ⟨{}⟩
 def insert (s : NameSet) (n : Name) : NameSet := Std.RBTree.insert s n
diff --git a/src/Lean/Data/NameTrie.lean b/src/Lean/Data/NameTrie.lean
index e932c5ebdb..113ee7e136 100644
--- a/src/Lean/Data/NameTrie.lean
+++ b/src/Lean/Data/NameTrie.lean
@@ -16,13 +16,19 @@ instance : ToString NamePart where
     | NamePart.str s => s
     | NamePart.num n => toString n
 
+def NamePart.cmp : NamePart → NamePart → Ordering
+  | NamePart.str a, NamePart.str b => compare a b
+  | NamePart.num a, NamePart.num b => compare a b
+  | NamePart.num _, NamePart.str _ => Ordering.lt
+  | _, _ => Ordering.gt
+
 def NamePart.lt : NamePart → NamePart → Bool
   | NamePart.str a, NamePart.str b => a < b
   | NamePart.num a, NamePart.num b => a < b
   | NamePart.num _, NamePart.str _ => true
   | _, _ => false
 
-def NameTrie (β : Type u) := PrefixTree NamePart β NamePart.lt
+def NameTrie (β : Type u) := PrefixTree NamePart β NamePart.cmp
 
 private def toKey (n : Name) : List NamePart :=
   loop n []
diff --git a/src/Lean/Data/PrefixTree.lean b/src/Lean/Data/PrefixTree.lean
index e02b3011f8..6f10c4eb76 100644
--- a/src/Lean/Data/PrefixTree.lean
+++ b/src/Lean/Data/PrefixTree.lean
@@ -21,7 +21,7 @@ def empty : PrefixTreeNode α β :=
   PrefixTreeNode.Node none RBNode.leaf
 
 @[specialize]
-partial def insert (t : PrefixTreeNode α β) (lt : α → α → Bool) (k : List α) (val : β) : PrefixTreeNode α β :=
+partial def insert (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) (val : β) : PrefixTreeNode α β :=
   let rec insertEmpty (k : List α) : PrefixTreeNode α β :=
     match k with
     | [] => PrefixTreeNode.Node (some val) RBNode.leaf
@@ -32,24 +32,24 @@ partial def insert (t : PrefixTreeNode α β) (lt : α → α → Bool) (k : Lis
     | PrefixTreeNode.Node v m, [] =>
       PrefixTreeNode.Node (some val) m -- overrides old value
     | PrefixTreeNode.Node v m, k :: ks =>
-      let t := match RBNode.find lt m k with
+      let t := match RBNode.find cmp m k with
         | none   => insertEmpty ks
         | some t => loop t ks
-      PrefixTreeNode.Node v (RBNode.insert lt m k t)
+      PrefixTreeNode.Node v (RBNode.insert cmp m k t)
   loop t k
 
 @[specialize]
-partial def find? (t : PrefixTreeNode α β) (lt : α → α → Bool) (k : List α) : Option β :=
+partial def find? (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) : Option β :=
   let rec loop
     | PrefixTreeNode.Node val m, [] => val
     | PrefixTreeNode.Node val m, k :: ks =>
-      match RBNode.find lt m k with
+      match RBNode.find cmp m k with
       | none   => none
       | some t => loop t ks
   loop t k
 
 @[specialize]
-partial def foldMatchingM [Monad m] (t : PrefixTreeNode α β) (lt : α → α → Bool) (k : List α) (init : σ) (f : β → σ → m σ) : m σ :=
+partial def foldMatchingM [Monad m] (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) (init : σ) (f : β → σ → m σ) : m σ :=
   let rec fold : PrefixTreeNode α β → σ → m σ
     | PrefixTreeNode.Node b? n, d => do
       let d ← match b? with
@@ -59,19 +59,19 @@ partial def foldMatchingM [Monad m] (t : PrefixTreeNode α β) (lt : α → α 
   let rec find : List α → PrefixTreeNode α β → σ → m σ
     | [],    t, d => fold t d
     | k::ks, PrefixTreeNode.Node _ m, d =>
-      match RBNode.find lt m k with
+      match RBNode.find cmp m k with
       | none   => pure init
       | some t => find ks t d
   find k t init
 
-inductive WellFormed (lt : α → α → Bool) : PrefixTreeNode α β → Prop where
-  | emptyWff    : WellFormed lt empty
-  | insertWff  {t : PrefixTreeNode α β} {k : List α} {val : β} : WellFormed lt t → WellFormed lt (insert t lt k val)
+inductive WellFormed (cmp : α → α → Ordering) : PrefixTreeNode α β → Prop where
+  | emptyWff    : WellFormed cmp empty
+  | insertWff  {t : PrefixTreeNode α β} {k : List α} {val : β} : WellFormed cmp t → WellFormed cmp (insert t cmp k val)
 
 end PrefixTreeNode
 
-def PrefixTree (α : Type u) (β : Type v) (lt : α → α → Bool) : Type (max u v) :=
-  { t : PrefixTreeNode α β // t.WellFormed lt }
+def PrefixTree (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Type (max u v) :=
+  { t : PrefixTreeNode α β // t.WellFormed cmp }
 
 open PrefixTreeNode
 
diff --git a/src/Lean/Data/Trie.lean b/src/Lean/Data/Trie.lean
index d879e29618..3d76ce4d8a 100644
--- a/src/Lean/Data/Trie.lean
+++ b/src/Lean/Data/Trie.lean
@@ -42,10 +42,10 @@ partial def insert (t : Trie α) (s : String) (val : α) : Trie α :=
       | false =>
         let c := s.get i
         let i := s.next i
-        let t := match RBNode.find (.<.) m c with
+        let t := match RBNode.find compare m c with
           | none   => insertEmpty i
           | some t => loop t i
-        Trie.Node v (RBNode.insert (.<.) m c t)
+        Trie.Node v (RBNode.insert compare m c t)
   loop t 0
 
 partial def find? (t : Trie α) (s : String) : Option α :=
@@ -56,7 +56,7 @@ partial def find? (t : Trie α) (s : String) : Option α :=
       | false =>
         let c := s.get i
         let i := s.next i
-        match RBNode.find (.<.) m c with
+        match RBNode.find compare m c with
         | none   => none
         | some t => loop t i
   loop t 0
@@ -75,7 +75,7 @@ partial def matchPrefix (s : String) (t : Trie α) (i : String.Pos) : String.Pos
         let acc := updtAcc v i acc
         let c   := s.get i
         let i   := s.next i
-        match RBNode.find (.<.) m c with
+        match RBNode.find compare m c with
         | some t => loop t i acc
         | none   => acc
   loop t i (i, none)
diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean
index 8c9f8fc345..3cd3ae4bf7 100644
--- a/src/Lean/Elab/Deriving/Inhabited.lean
+++ b/src/Lean/Elab/Deriving/Inhabited.lean
@@ -9,7 +9,7 @@ namespace Lean.Elab
 open Command
 open Meta
 
-private abbrev IndexSet := Std.RBTree Nat (.<.)
+private abbrev IndexSet := Std.RBTree Nat compare
 private abbrev LocalInst2Index := NameMap Nat
 
 private def implicitBinderF := Parser.Term.implicitBinder
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index 59aeb54f07..065460fa71 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -77,7 +77,7 @@ structure DefaultInstanceEntry where
   instanceName : Name
   priority     : Nat
 
-abbrev PrioritySet := Std.RBTree Nat (.>.)
+abbrev PrioritySet := Std.RBTree Nat (fun x y => compare y x)
 
 structure DefaultInstances where
   defaultInstances : NameMap (List (Name × Nat)) := {}
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index c7c624f2ea..73cde06e62 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1535,7 +1535,7 @@ def eoiFn : ParserFn := fun c s =>
 open Std (RBMap RBMap.empty)
 
 /-- A multimap indexed by tokens. Used for indexing parsers by their leading token. -/
-def TokenMap (α : Type) := RBMap Name (List α) Name.quickLt
+def TokenMap (α : Type) := RBMap Name (List α) Name.quickCmp
 
 namespace TokenMap
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index 3c37a516bd..c82d6b2c93 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -165,7 +165,7 @@ def getPPUnicode (o : Options) : Bool := o.get `pp.unicode true
 def getPPSafeShadowing (o : Options) : Bool := o.get `pp.safe_shadowing true
 
 /-- Associate pretty printer options to a specific subterm using a synthetic position. -/
-abbrev OptionsPerPos := Std.RBMap Nat Options (fun a b => a < b)
+abbrev OptionsPerPos := Std.RBMap Nat Options compare
 
 namespace PrettyPrinter
 namespace Delaborator
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index e2e7ebb93d..946e34da5c 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -150,7 +150,7 @@ section Elab
 end Elab
 
 -- Pending requests are tracked so they can be cancelled
-abbrev PendingRequestMap := RBMap RequestID (Task (Except IO.Error Unit)) (fun a b => Decidable.decide (a < b))
+abbrev PendingRequestMap := RBMap RequestID (Task (Except IO.Error Unit)) compare
 
 structure ServerContext where
   hIn                : FS.Stream
diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
index e10edeabfb..3b2e05919e 100644
--- a/src/Lean/Server/Watchdog.lean
+++ b/src/Lean/Server/Watchdog.lean
@@ -96,7 +96,7 @@ section Utils
     | crashed (queuedMsgs : Array JsonRpc.Message)
     | running
 
-  abbrev PendingRequestMap := RBMap RequestID JsonRpc.Message (fun a b => Decidable.decide (a < b))
+  abbrev PendingRequestMap := RBMap RequestID JsonRpc.Message compare
 
   private def parseHeaderAst (input : String) : IO Syntax := do
     let inputCtx   := Parser.mkInputContext input "<input>"
@@ -166,7 +166,7 @@ section FileWorker
 end FileWorker
 
 section ServerM
-  abbrev FileWorkerMap := RBMap DocumentUri FileWorker (fun a b => Decidable.decide (a < b))
+  abbrev FileWorkerMap := RBMap DocumentUri FileWorker compare
 
   structure ServerContext where
     hIn            : FS.Stream
diff --git a/src/Std/Data/RBMap.lean b/src/Std/Data/RBMap.lean
index 682dcb4027..ebeeca1c4c 100644
--- a/src/Std/Data/RBMap.lean
+++ b/src/Std/Data/RBMap.lean
@@ -94,31 +94,32 @@ def isBlack : RBNode α β → Bool
 
 section Insert
 
-variable (lt : α → α → Bool)
+variable (cmp : α → α → Ordering)
 
 @[specialize] def ins : RBNode α β → (k : α) → β k → RBNode α β
   | leaf,               kx, vx => node red leaf kx vx leaf
   | node red a ky vy b, kx, vx =>
-     if lt kx ky then node red (ins a kx vx) ky vy b
-     else if lt ky kx then node red a ky vy (ins b kx vx)
-     else node red a kx vx b
+    match cmp kx ky with
+    | Ordering.lt => node red (ins a kx vx) ky vy b
+    | Ordering.gt => node red a ky vy (ins b kx vx)
+    | Ordering.eq => node red a kx vx b
   | node black a ky vy b, kx, vx =>
-      if lt kx ky then
-        if isRed a then balance1 ky vy b (ins a kx vx)
+    match cmp kx ky with
+    | Ordering.lt => 
+      if isRed a then balance1 ky vy b (ins a kx vx)
         else node black (ins a kx vx) ky vy b
-      else if lt ky kx then
+    | Ordering.gt =>
         if isRed b then balance2 a ky vy (ins b kx vx)
         else node black a ky vy (ins b kx vx)
-      else
-         node black a kx vx b
+    | Ordering.eq => node black a kx vx b
 
 def setBlack : RBNode α β → RBNode α β
   | node _ l k v r => node black l k v r
   | e              => e
 
 @[specialize] def insert (t : RBNode α β) (k : α) (v : β k) : RBNode α β :=
-  if isRed t then setBlack (ins lt t k v)
-  else ins lt t k v
+  if isRed t then setBlack (ins cmp t k v)
+  else ins cmp t k v
 
 end Insert
 
@@ -166,55 +167,59 @@ partial def appendTrees :  RBNode α β → RBNode α β → RBNode α β
 
 section Erase
 
-variable (lt : α → α → Bool)
+variable (cmp : α → α → Ordering)
 
 @[specialize] def del (x : α) : RBNode α β → RBNode α β
   | leaf           => leaf
   | node _ a y v b =>
-    if lt x y then
+    match cmp x y with
+    | Ordering.lt =>
       if a.isBlack then balLeft (del x a) y v b
       else node red (del x a) y v b
-    else if lt y x then
+    | Ordering.gt =>
       if b.isBlack then balRight a y v (del x b)
       else node red a y v (del x b)
-    else appendTrees a b
+    | Ordering.eq => appendTrees a b
 
 @[specialize] def erase (x : α) (t : RBNode α β) : RBNode α β :=
-  let t := del lt x t;
+  let t := del cmp x t;
   t.setBlack
 
 end Erase
 
 section Membership
-variable (lt : α → α → Bool)
+variable (cmp : α → α → Ordering)
 
 @[specialize] def findCore : RBNode α β → (k : α) → Option (Sigma (fun k => β k))
   | leaf,             x => none
   | node _ a ky vy b, x =>
-     if lt x ky then findCore a x
-     else if lt ky x then findCore b x
-     else some ⟨ky, vy⟩
+    match cmp x ky with
+    | Ordering.lt => findCore a x
+    | Ordering.gt => findCore b x
+    | Ordering.eq => some ⟨ky, vy⟩
 
 @[specialize] def find {β : Type v} : RBNode α (fun _ => β) → α → Option β
   | leaf,             x => none
   | node _ a ky vy b, x =>
-    if lt x ky then find a x
-    else if lt ky x then find b x
-    else some vy
+    match cmp x ky with
+    | Ordering.lt => find a x
+    | Ordering.gt => find b x
+    | Ordering.eq => some vy
 
 @[specialize] def lowerBound : RBNode α β → α → Option (Sigma β) → Option (Sigma β)
   | leaf,             x, lb => lb
   | node _ a ky vy b, x, lb =>
-    if lt x ky then lowerBound a x lb
-    else if lt ky x then lowerBound b x (some ⟨ky, vy⟩)
-    else some ⟨ky, vy⟩
+    match cmp x ky with
+    | Ordering.lt => lowerBound a x lb
+    | Ordering.gt => lowerBound b x (some ⟨ky, vy⟩)
+    | Ordering.eq => some ⟨ky, vy⟩
 
 end Membership
 
-inductive WellFormed (lt : α → α → Bool) : RBNode α β → Prop where
-  | leafWff : WellFormed lt leaf
-  | insertWff {n n' : RBNode α β} {k : α} {v : β k} : WellFormed lt n → n' = insert lt n k v → WellFormed lt n'
-  | eraseWff {n n' : RBNode α β} {k : α} : WellFormed lt n → n' = erase lt k n → WellFormed lt n'
+inductive WellFormed (cmp : α → α → Ordering) : RBNode α β → Prop where
+  | leafWff : WellFormed cmp leaf
+  | insertWff {n n' : RBNode α β} {k : α} {v : β k} : WellFormed cmp n → n' = insert cmp n k v → WellFormed cmp n'
+  | eraseWff {n n' : RBNode α β} {k : α} : WellFormed cmp n → n' = erase cmp k n → WellFormed cmp n'
 
 end RBNode
 
@@ -222,124 +227,124 @@ open Std.RBNode
 
 /- TODO(Leo): define dRBMap -/
 
-def RBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : Type (max u v) :=
-  {t : RBNode α (fun _ => β) // t.WellFormed lt }
+def RBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Type (max u v) :=
+  {t : RBNode α (fun _ => β) // t.WellFormed cmp }
 
-@[inline] def mkRBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : RBMap α β lt :=
+@[inline] def mkRBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : RBMap α β cmp :=
   ⟨leaf, WellFormed.leafWff⟩
 
-@[inline] def RBMap.empty {α : Type u} {β : Type v} {lt : α → α → Bool} : RBMap α β lt :=
+@[inline] def RBMap.empty {α : Type u} {β : Type v} {cmp : α → α → Ordering} : RBMap α β cmp :=
   mkRBMap ..
 
-instance (α : Type u) (β : Type v) (lt : α → α → Bool) : EmptyCollection (RBMap α β lt) :=
+instance (α : Type u) (β : Type v) (cmp : α → α → Ordering) : EmptyCollection (RBMap α β cmp) :=
   ⟨RBMap.empty⟩
 
 namespace RBMap
-variable {α : Type u} {β : Type v} {σ : Type w} {lt : α → α → Bool}
+variable {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering}
 
-def depth (f : Nat → Nat → Nat) (t : RBMap α β lt) : Nat :=
+def depth (f : Nat → Nat → Nat) (t : RBMap α β cmp) : Nat :=
   t.val.depth f
 
-@[inline] def fold (f : σ → α → β → σ) : (init : σ) → RBMap α β lt → σ
+@[inline] def fold (f : σ → α → β → σ) : (init : σ) → RBMap α β cmp → σ
   | b, ⟨t, _⟩ => t.fold f b
 
-@[inline] def revFold (f : σ → α → β → σ) : (init : σ) → RBMap α β lt → σ
+@[inline] def revFold (f : σ → α → β → σ) : (init : σ) → RBMap α β cmp → σ
   | b, ⟨t, _⟩ => t.revFold f b
 
-@[inline] def foldM [Monad m] (f : σ → α → β → m σ) : (init : σ) → RBMap α β lt → m σ
+@[inline] def foldM [Monad m] (f : σ → α → β → m σ) : (init : σ) → RBMap α β cmp → m σ
   | b, ⟨t, _⟩ => t.foldM f b
 
-@[inline] def forM [Monad m] (f : α → β → m PUnit) (t : RBMap α β lt) : m PUnit :=
+@[inline] def forM [Monad m] (f : α → β → m PUnit) (t : RBMap α β cmp) : m PUnit :=
   t.foldM (fun _ k v => f k v) ⟨⟩
 
-@[inline] protected def forIn [Monad m] (t : RBMap α β lt) (init : σ) (f : (α × β) → σ → m (ForInStep σ)) : m σ :=
+@[inline] protected def forIn [Monad m] (t : RBMap α β cmp) (init : σ) (f : (α × β) → σ → m (ForInStep σ)) : m σ :=
   t.val.forIn init (fun a b acc => f (a, b) acc)
 
-instance : ForIn m (RBMap α β lt) (α × β) where
+instance : ForIn m (RBMap α β cmp) (α × β) where
   forIn := RBMap.forIn
 
-@[inline] def isEmpty : RBMap α β lt → Bool
+@[inline] def isEmpty : RBMap α β cmp → Bool
   | ⟨leaf, _⟩ => true
   | _         => false
 
-@[specialize] def toList : RBMap α β lt → List (α × β)
+@[specialize] def toList : RBMap α β cmp → List (α × β)
   | ⟨t, _⟩ => t.revFold (fun ps k v => (k, v)::ps) []
 
-@[inline] protected def min : RBMap α β lt → Option (α × β)
+@[inline] protected def min : RBMap α β cmp → Option (α × β)
   | ⟨t, _⟩ =>
     match t.min with
     | some ⟨k, v⟩ => some (k, v)
     | none        => none
 
-@[inline] protected def max : RBMap α β lt → Option (α × β)
+@[inline] protected def max : RBMap α β cmp → Option (α × β)
   | ⟨t, _⟩ =>
     match t.max with
     | some ⟨k, v⟩ => some (k, v)
     | none        => none
 
-instance [Repr α] [Repr β] : Repr (RBMap α β lt) where
+instance [Repr α] [Repr β] : Repr (RBMap α β cmp) where
   reprPrec m prec := Repr.addAppParen ("Std.rbmapOf " ++ repr m.toList) prec
 
-@[inline] def insert : RBMap α β lt → α → β → RBMap α β lt
-  | ⟨t, w⟩, k, v => ⟨t.insert lt k v, WellFormed.insertWff w rfl⟩
+@[inline] def insert : RBMap α β cmp → α → β → RBMap α β cmp
+  | ⟨t, w⟩, k, v => ⟨t.insert cmp k v, WellFormed.insertWff w rfl⟩
 
-@[inline] def erase : RBMap α β lt → α → RBMap α β lt
-  | ⟨t, w⟩, k => ⟨t.erase lt k, WellFormed.eraseWff w rfl⟩
+@[inline] def erase : RBMap α β cmp → α → RBMap α β cmp
+  | ⟨t, w⟩, k => ⟨t.erase cmp k, WellFormed.eraseWff w rfl⟩
 
-@[specialize] def ofList : List (α × β) → RBMap α β lt
+@[specialize] def ofList : List (α × β) → RBMap α β cmp
   | []        => mkRBMap ..
   | ⟨k,v⟩::xs => (ofList xs).insert k v
 
-@[inline] def findCore? : RBMap α β lt → α → Option (Sigma (fun (k : α) => β))
-  | ⟨t, _⟩, x => t.findCore lt x
+@[inline] def findCore? : RBMap α β cmp → α → Option (Sigma (fun (k : α) => β))
+  | ⟨t, _⟩, x => t.findCore cmp x
 
-@[inline] def find? : RBMap α β lt → α → Option β
-  | ⟨t, _⟩, x => t.find lt x
+@[inline] def find? : RBMap α β cmp → α → Option β
+  | ⟨t, _⟩, x => t.find cmp x
 
-@[inline] def findD (t : RBMap α β lt) (k : α) (v₀ : β) : β :=
+@[inline] def findD (t : RBMap α β cmp) (k : α) (v₀ : β) : β :=
   (t.find? k).getD v₀
 
 /-- (lowerBound k) retrieves the kv pair of the largest key smaller than or equal to `k`,
     if it exists. -/
-@[inline] def lowerBound : RBMap α β lt → α → Option (Sigma (fun (k : α) => β))
-  | ⟨t, _⟩, x => t.lowerBound lt x none
+@[inline] def lowerBound : RBMap α β cmp → α → Option (Sigma (fun (k : α) => β))
+  | ⟨t, _⟩, x => t.lowerBound cmp x none
 
-@[inline] def contains (t : RBMap α β lt) (a : α) : Bool :=
+@[inline] def contains (t : RBMap α β cmp) (a : α) : Bool :=
   (t.find? a).isSome
 
-@[inline] def fromList (l : List (α × β)) (lt : α → α → Bool) : RBMap α β lt :=
-  l.foldl (fun r p => r.insert p.1 p.2) (mkRBMap α β lt)
+@[inline] def fromList (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=
+  l.foldl (fun r p => r.insert p.1 p.2) (mkRBMap α β cmp)
 
-@[inline] def all : RBMap α β lt → (α → β → Bool) → Bool
+@[inline] def all : RBMap α β cmp → (α → β → Bool) → Bool
   | ⟨t, _⟩, p => t.all p
 
-@[inline] def any : RBMap α β lt → (α → β → Bool) → Bool
+@[inline] def any : RBMap α β cmp → (α → β → Bool) → Bool
   | ⟨t, _⟩, p => t.any p
 
-def size (m : RBMap α β lt) : Nat :=
+def size (m : RBMap α β cmp) : Nat :=
   m.fold (fun sz _ _ => sz+1) 0
 
-def maxDepth (t : RBMap α β lt) : Nat :=
+def maxDepth (t : RBMap α β cmp) : Nat :=
   t.val.depth Nat.max
 
-@[inline] def min! [Inhabited α] [Inhabited β] (t : RBMap α β lt) : α × β :=
+@[inline] def min! [Inhabited α] [Inhabited β] (t : RBMap α β cmp) : α × β :=
   match t.min with
   | some p => p
   | none   => panic! "map is empty"
 
-@[inline] def max! [Inhabited α] [Inhabited β] (t : RBMap α β lt) : α × β :=
+@[inline] def max! [Inhabited α] [Inhabited β] (t : RBMap α β cmp) : α × β :=
   match t.max with
   | some p => p
   | none   => panic! "map is empty"
 
-@[inline] def find! [Inhabited β] (t : RBMap α β lt) (k : α) : β :=
+@[inline] def find! [Inhabited β] (t : RBMap α β cmp) (k : α) : β :=
   match t.find? k with
   | some b => b
   | none   => panic! "key is not in the map"
 
 end RBMap
 
-def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Bool) : RBMap α β lt :=
-  RBMap.fromList l lt
+def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp :=
+  RBMap.fromList l cmp
 
 end Std
diff --git a/src/Std/Data/RBTree.lean b/src/Std/Data/RBTree.lean
index 24fbab418e..292bdae34f 100644
--- a/src/Std/Data/RBTree.lean
+++ b/src/Std/Data/RBTree.lean
@@ -7,99 +7,99 @@ import Std.Data.RBMap
 namespace Std
 universes u v w
 
-def RBTree (α : Type u) (lt : α → α → Bool) : Type u :=
-  RBMap α Unit lt
+def RBTree (α : Type u) (cmp : α → α → Ordering) : Type u :=
+  RBMap α Unit cmp
 
 instance : Inhabited (RBTree α p) where
   default := RBMap.empty
 
-@[inline] def mkRBTree (α : Type u) (lt : α → α → Bool) : RBTree α lt :=
-  mkRBMap α Unit lt
+@[inline] def mkRBTree (α : Type u) (cmp : α → α → Ordering) : RBTree α cmp :=
+  mkRBMap α Unit cmp
 
-instance (α : Type u) (lt : α → α → Bool) : EmptyCollection (RBTree α lt) :=
-  ⟨mkRBTree α lt⟩
+instance (α : Type u) (cmp : α → α → Ordering) : EmptyCollection (RBTree α cmp) :=
+  ⟨mkRBTree α cmp⟩
 
 namespace RBTree
-variable {α : Type u} {β : Type v} {lt : α → α → Bool}
+variable {α : Type u} {β : Type v} {cmp : α → α → Ordering}
 
-@[inline] def empty : RBTree α lt :=
+@[inline] def empty : RBTree α cmp :=
   RBMap.empty
 
-@[inline] def depth (f : Nat → Nat → Nat) (t : RBTree α lt) : Nat :=
+@[inline] def depth (f : Nat → Nat → Nat) (t : RBTree α cmp) : Nat :=
   RBMap.depth f t
 
-@[inline] def fold (f : β → α → β) (init : β) (t : RBTree α lt) : β :=
+@[inline] def fold (f : β → α → β) (init : β) (t : RBTree α cmp) : β :=
   RBMap.fold (fun r a _ => f r a) init t
 
-@[inline] def revFold (f : β → α → β) (init : β) (t : RBTree α lt) : β :=
+@[inline] def revFold (f : β → α → β) (init : β) (t : RBTree α cmp) : β :=
   RBMap.revFold (fun r a _ => f r a) init t
 
-@[inline] def foldM {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (t : RBTree α lt) : m β :=
+@[inline] def foldM {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (t : RBTree α cmp) : m β :=
   RBMap.foldM (fun r a _ => f r a) init t
 
-@[inline] def forM {m : Type v → Type w} [Monad m] (f : α → m PUnit) (t : RBTree α lt) : m PUnit :=
+@[inline] def forM {m : Type v → Type w} [Monad m] (f : α → m PUnit) (t : RBTree α cmp) : m PUnit :=
   t.foldM (fun _ a => f a) ⟨⟩
 
-@[inline] protected def forIn [Monad m] (t : RBTree α lt) (init : σ) (f : α → σ → m (ForInStep σ)) : m σ :=
+@[inline] protected def forIn [Monad m] (t : RBTree α cmp) (init : σ) (f : α → σ → m (ForInStep σ)) : m σ :=
   t.val.forIn init (fun a _ acc => f a acc)
 
-instance : ForIn m (RBTree α lt) α where
+instance : ForIn m (RBTree α cmp) α where
   forIn := RBTree.forIn
 
-@[inline] def isEmpty (t : RBTree α lt) : Bool :=
+@[inline] def isEmpty (t : RBTree α cmp) : Bool :=
   RBMap.isEmpty t
 
-@[specialize] def toList (t : RBTree α lt) : List α :=
+@[specialize] def toList (t : RBTree α cmp) : List α :=
   t.revFold (fun as a => a::as) []
 
-@[inline] protected def min (t : RBTree α lt) : Option α :=
+@[inline] protected def min (t : RBTree α cmp) : Option α :=
   match RBMap.min t with
   | some ⟨a, _⟩ => some a
   | none        => none
 
-@[inline] protected def max (t : RBTree α lt) : Option α :=
+@[inline] protected def max (t : RBTree α cmp) : Option α :=
   match RBMap.max t with
   | some ⟨a, _⟩ => some a
   | none        => none
 
-instance [Repr α] : Repr (RBTree α lt) where
+instance [Repr α] : Repr (RBTree α cmp) where
   reprPrec t prec := Repr.addAppParen ("Std.rbtreeOf " ++ repr t.toList) prec
 
-@[inline] def insert (t : RBTree α lt) (a : α) : RBTree α lt :=
+@[inline] def insert (t : RBTree α cmp) (a : α) : RBTree α cmp :=
   RBMap.insert t a ()
 
-@[inline] def erase (t : RBTree α lt) (a : α) : RBTree α lt :=
+@[inline] def erase (t : RBTree α cmp) (a : α) : RBTree α cmp :=
   RBMap.erase t a
 
-@[specialize] def ofList : List α → RBTree α lt
+@[specialize] def ofList : List α → RBTree α cmp
   | []    => mkRBTree ..
   | x::xs => (ofList xs).insert x
 
-@[inline] def find? (t : RBTree α lt) (a : α) : Option α :=
+@[inline] def find? (t : RBTree α cmp) (a : α) : Option α :=
   match RBMap.findCore? t a with
   | some ⟨a, _⟩ => some a
   | none        => none
 
-@[inline] def contains (t : RBTree α lt) (a : α) : Bool :=
+@[inline] def contains (t : RBTree α cmp) (a : α) : Bool :=
   (t.find? a).isSome
 
-def fromList (l : List α) (lt : α → α → Bool) : RBTree α lt :=
-  l.foldl insert (mkRBTree α lt)
+def fromList (l : List α) (cmp : α → α → Ordering) : RBTree α cmp :=
+  l.foldl insert (mkRBTree α cmp)
 
-@[inline] def all (t : RBTree α lt) (p : α → Bool) : Bool :=
+@[inline] def all (t : RBTree α cmp) (p : α → Bool) : Bool :=
   RBMap.all t (fun a _ => p a)
 
-@[inline] def any (t : RBTree α lt) (p : α → Bool) : Bool :=
+@[inline] def any (t : RBTree α cmp) (p : α → Bool) : Bool :=
   RBMap.any t (fun a _ => p a)
 
-def subset (t₁ t₂ : RBTree α lt) : Bool :=
+def subset (t₁ t₂ : RBTree α cmp) : Bool :=
   t₁.all fun a => (t₂.find? a).toBool
 
-def seteq (t₁ t₂ : RBTree α lt) : Bool :=
+def seteq (t₁ t₂ : RBTree α cmp) : Bool :=
   subset t₁ t₂ && subset t₂ t₁
 
 end RBTree
 
-def rbtreeOf {α : Type u} (l : List α) (lt : α → α → Bool) : RBTree α lt :=
-  RBTree.fromList l lt
+def rbtreeOf {α : Type u} (l : List α) (cmp : α → α → Ordering) : RBTree α cmp :=
+  RBTree.fromList l cmp
 end Std
diff --git a/tests/compiler/rbmap_library.lean b/tests/compiler/rbmap_library.lean
index 54844b7f18..cba7ac5c54 100644
--- a/tests/compiler/rbmap_library.lean
+++ b/tests/compiler/rbmap_library.lean
@@ -4,14 +4,14 @@ open Std
 def check (b : Bool) : IO Unit := do
 unless b do IO.println "ERROR"
 
-def sz {α β : Type} {lt : α → α → Bool} (m : RBMap α β lt) : Nat :=
+def sz {α β : Type} {cmp : α → α → Ordering} (m : RBMap α β cmp) : Nat :=
 m.fold (fun sz _ _ => sz+1) 0
 
-def depth {α β : Type} {lt : α → α → Bool} (m : RBMap α β lt) : Nat :=
+def depth {α β : Type} {cmp : α → α → Ordering} (m : RBMap α β cmp) : Nat :=
 m.depth Nat.max
 
 def tst1 : IO Unit :=
-do let Map := RBMap String Nat (fun a b => a < b)
+do let Map := RBMap String Nat compare
    let m : Map := {}
    let m := m.insert "hello" 0
    let m := m.insert "world" 1
@@ -23,7 +23,7 @@ do let Map := RBMap String Nat (fun a b => a < b)
    pure ()
 
 def tst2 : IO Unit :=
-do let Map := RBMap Nat Nat (fun a b => a < b)
+do let Map := RBMap Nat Nat compare
    let m : Map := {}
    let n : Nat := 10000
    let mut m := n.fold (fun i (m : Map) => m.insert i (i*10)) m
@@ -37,7 +37,7 @@ do let Map := RBMap Nat Nat (fun a b => a < b)
    IO.println (">> " ++ toString (depth m) ++ ", " ++ toString (sz m))
    pure ()
 
-abbrev Map := RBMap Nat Nat (fun a b => a < b)
+abbrev Map := RBMap Nat Nat compare
 
 def mkRandMap (max : Nat) : Nat → Map → Array (Nat × Nat) → IO (Map × Array (Nat × Nat))
 | 0,     m, a => pure (m, a)