fix: typo at sameHeadSymbol

see #1190
2022-06-06 07:46:57 -07:00 · 2022-06-06 07:46:57 -07:00 · 22281f25c8
commit 22281f25c8
parent 7428dc5e71
1 changed files with 1 additions and 1 deletions
--- 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

 /--