From ede8a7e4942affd4e841f13c941688f18d2a5fcc Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Mon, 30 Jun 2025 07:10:04 +0200
Subject: [PATCH] fix: error explanation needs updating (#9091)

This PR updates an error explanation to match the actual error.
---
 src/Lean/ErrorExplanations/InvalidDottedIdent.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/ErrorExplanations/InvalidDottedIdent.lean b/src/Lean/ErrorExplanations/InvalidDottedIdent.lean
index ef9989f7b1..6eaa6f0001 100644
--- a/src/Lean/ErrorExplanations/InvalidDottedIdent.lean
+++ b/src/Lean/ErrorExplanations/InvalidDottedIdent.lean
@@ -25,7 +25,7 @@ def reverseDuplicate (xs : List α) :=
   .reverse (xs ++ xs)
 ```
 ```output
-Invalid dotted identifier notation: The type of `.reverse` could not be determined
+Invalid dotted identifier notation: The expected type of `.reverse` could not be determined
 ```
 ```lean fixed
 def reverseDuplicate (xs : List α) : List α :=