From 22281f25c874dab350d3cc2041cfc0efaf655ecd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 6 Jun 2022 07:46:57 -0700
Subject: [PATCH] fix: typo at `sameHeadSymbol`

see #1190
---
 src/Lean/Meta/ExprDefEq.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 84826e3b4f..0dc5b84095 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1147,7 +1147,7 @@ private def unfoldBothDefEq (fn : Name) (t s : Expr) : MetaM LBool := do
 
 private def sameHeadSymbol (t s : Expr) : Bool :=
   match t.getAppFn, s.getAppFn with
-  | Expr.const c₁ _ _, Expr.const c₂ _ _ => true
+  | Expr.const c₁ _ _, Expr.const c₂ _ _ => c₁ == c₂
   | _,                 _                 => false
 
 /--