max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: error explanation needs updating (#9091)

Browse source 
This PR updates an error explanation to match the actual error.
This commit is contained in:
David Thrane Christiansen 2025-06-30 07:10:04 +02:00 • committed by GitHub
parent 044bfdb098
commit ede8a7e494
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/ErrorExplanations/InvalidDottedIdent.lean
View file

@ -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 α :=