chore: replace DecidableEq Name with HasBeq Name

library/Init/Data/List/Basic.lean

@@ -335,4 +335,12 @@ isPrefixOf l₁.reverse l₂.reverse
 | [],    [],    _   => true
 | a::as, b::bs, eqv => eqv a b && isEqv as bs eqv
 | _,     _,     eqv => false
+
+protected def beq [HasBeq α] : List α → List α → Bool
+| [],    []    => true
+| a::as, b::bs => a == b && beq as bs
+| _,     _     => false
+
+instance [HasBeq α] : HasBeq (List α) := ⟨List.beq⟩
+
 end List

library/Init/Lean/Compiler/ConstFolding.lean

@@ -31,15 +31,15 @@ def numScalarTypes : List NumScalarTypeInfo :=
  {id := `USize, nbits := System.Platform.numBits}]
 
 def isOfNat (fn : Name) : Bool :=
-numScalarTypes.any (fun info => info.ofNatFn = fn)
+numScalarTypes.any (fun info => info.ofNatFn == fn)
 
 def isToNat (fn : Name) : Bool :=
-numScalarTypes.any (fun info => info.toNatFn = fn)
+numScalarTypes.any (fun info => info.toNatFn == fn)
 
 def getInfoFromFn (fn : Name) : List NumScalarTypeInfo → Option NumScalarTypeInfo
 | []          => none
 | info::infos =>
-  if info.ofNatFn = fn then some info
+  if info.ofNatFn == fn then some info
   else getInfoFromFn infos
 
 def getInfoFromVal : Expr → Option NumScalarTypeInfo

library/Init/Lean/Compiler/ExternAttr.lean

@@ -133,8 +133,8 @@ def ExternEntry.backend : ExternEntry → Name
 def getExternEntryForAux (backend : Name) : List ExternEntry → Option ExternEntry
 | []    => none
 | e::es =>
-  if e.backend = `all then some e
-  else if e.backend = backend then some e
+  if e.backend == `all then some e
+  else if e.backend == backend then some e
   else getExternEntryForAux es
 
 def getExternEntryFor (d : ExternAttrData) (backend : Name) : Option ExternEntry :=

library/Init/Lean/KVMap.lean

@@ -46,7 +46,7 @@ def isEmpty : KVMap → Bool
 
 def findCore : List (Name × DataValue) → Name → Option DataValue
 | [],       k' => none
-| (k,v)::m, k' => if k = k' then some v else findCore m k'
+| (k,v)::m, k' => if k == k' then some v else findCore m k'
 
 def find : KVMap → Name → Option DataValue
 | ⟨m⟩, k => findCore m k
@@ -56,7 +56,7 @@ def findD (m : KVMap) (k : Name) (d₀ : DataValue) : DataValue :=
 
 def insertCore : List (Name × DataValue) → Name → DataValue → List (Name × DataValue)
 | [],       k', v' => [(k',v')]
-| (k,v)::m, k', v' => if k = k' then (k, v') :: m else (k, v) :: insertCore m k' v'
+| (k,v)::m, k', v' => if k == k' then (k, v') :: m else (k, v) :: insertCore m k' v'
 
 def insert : KVMap → Name → DataValue → KVMap
 | ⟨m⟩, k, v => ⟨insertCore m k v⟩

library/Init/Lean/Name.lean

@@ -66,30 +66,13 @@ def components' : Name → List Name
 def components (n : Name) : List Name :=
 n.components'.reverse
 
-@[extern "lean_name_dec_eq"]
-protected def decEq : ∀ (a b : @& Name), Decidable (a = b)
-| anonymous,        anonymous        => isTrue rfl
-| mkString p₁ s₁,  mkString p₂ s₂  =>
-  if h₁ : s₁ = s₂ then
-    match decEq p₁ p₂ with
-    | isTrue h₂  => isTrue $ h₁ ▸ h₂ ▸ rfl
-    | isFalse h₂ => isFalse $ fun h => Name.noConfusion h $ fun hp hs => absurd hp h₂
-  else isFalse $ fun h => Name.noConfusion h $ fun hp hs => absurd hs h₁
-| mkNumeral p₁ n₁, mkNumeral p₂ n₂ =>
-  if h₁ : n₁ = n₂ then
-    match decEq p₁ p₂ with
-    | isTrue h₂  => isTrue $ h₁ ▸ h₂ ▸ rfl
-    | isFalse h₂ => isFalse $ fun h => Name.noConfusion h $ fun hp hs => absurd hp h₂
-  else isFalse $ fun h => Name.noConfusion h $ fun hp hs => absurd hs h₁
-| anonymous,       mkString _ _    => isFalse $ fun h => Name.noConfusion h
-| anonymous,       mkNumeral _ _   => isFalse $ fun h => Name.noConfusion h
-| mkString _ _,    anonymous       => isFalse $ fun h => Name.noConfusion h
-| mkString _ _,    mkNumeral _ _   => isFalse $ fun h => Name.noConfusion h
-| mkNumeral _ _,   anonymous       => isFalse $ fun h => Name.noConfusion h
-| mkNumeral _ _,   mkString _ _    => isFalse $ fun h => Name.noConfusion h
+protected def beq : Name → Name → Bool
+| anonymous,       anonymous       => true
+| mkString p₁ s₁,  mkString p₂ s₂  => s₁ == s₂ && beq p₁ p₂
+| mkNumeral p₁ n₁, mkNumeral p₂ n₂ => n₁ == n₂ && beq p₁ p₂
+| _,               _               => false
 
-instance : DecidableEq Name :=
-{decEq := Name.decEq}
+instance : HasBeq Name := ⟨Name.beq⟩
 
 def eqStr : Name → String → Bool
 | mkString Name.anonymous s,   s' => s == s'
@@ -109,12 +92,12 @@ def replacePrefix : Name → Name → Name → Name
 | anonymous, anonymous, newP => newP
 | anonymous, _,         _     => anonymous
 | n@(mkString p s), queryP, newP =>
-  if n = queryP then
+  if n == queryP then
     newP
   else
     mkString (p.replacePrefix queryP newP) s
 | n@(mkNumeral p s), queryP, newP =>
-  if n = queryP then
+  if n == queryP then
     newP
   else
     mkNumeral (p.replacePrefix queryP newP) s

library/Init/Lean/Syntax.lean

@@ -308,7 +308,7 @@ protected partial def formatStx {α} : Syntax α → Format
 | atom info val     => format $ repr val
 | ident _ _ val pre => format "`" ++ format val
 | node kind args    =>
-  if kind = `Lean.Parser.noKind then
+  if kind == `Lean.Parser.noKind then
     sbracket $ joinSep (args.toList.map formatStx) line
   else
     let shorterName := kind.replacePrefix `Lean.Parser Name.anonymous;

library/Init/Lean/TypeClass/Context.lean

@@ -154,7 +154,7 @@ partial def uUnify : Level → Level → EStateM String Context Unit
   else
     match l₁, l₂ with
     | Level.zero _,         Level.zero _         => pure ()
-    | Level.param p₁ _,     Level.param p₂ _     => when (p₁ ≠ p₂) $ throw "Level.param clash"
+    | Level.param p₁ _,     Level.param p₂ _     => when (p₁ != p₂) $ throw "Level.param clash"
     | Level.succ  l₁ _,     Level.succ  l₂ _     => uUnify l₁ l₂
     | Level.max l₁₁ l₁₂ _,  Level.max l₂₁ l₂₂ _  => uUnify l₁₁ l₂₁ *> uUnify l₁₂ l₂₂
     | Level.imax l₁₁ l₁₂ _, Level.imax l₂₁ l₂₂ _ => uUnify l₁₁ l₂₁ *> uUnify l₁₂ l₂₂