diff --git a/library/Init/Data/List/Basic.lean b/library/Init/Data/List/Basic.lean index 2db35a723b..a9e50cd84f 100644 --- a/library/Init/Data/List/Basic.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/ConstFolding.lean b/library/Init/Lean/Compiler/ConstFolding.lean index 7329880b63..a65a95d4ec 100644 --- a/library/Init/Lean/Compiler/ConstFolding.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/ExternAttr.lean b/library/Init/Lean/Compiler/ExternAttr.lean index 59671cc251..75a402f9ee 100644 --- a/library/Init/Lean/Compiler/ExternAttr.lean +++ b/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 := diff --git a/library/Init/Lean/KVMap.lean b/library/Init/Lean/KVMap.lean index 641f0ee3fd..9a1bbd79c6 100644 --- a/library/Init/Lean/KVMap.lean +++ b/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⟩ diff --git a/library/Init/Lean/Name.lean b/library/Init/Lean/Name.lean index 9a0545129f..f872640561 100644 --- a/library/Init/Lean/Name.lean +++ b/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 diff --git a/library/Init/Lean/Syntax.lean b/library/Init/Lean/Syntax.lean index a2e4ff0ed9..60e9d1eb35 100644 --- a/library/Init/Lean/Syntax.lean +++ b/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; diff --git a/library/Init/Lean/TypeClass/Context.lean b/library/Init/Lean/TypeClass/Context.lean index ea03958f96..50361c0226 100644 --- a/library/Init/Lean/TypeClass/Context.lean +++ b/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₂₂