Skip to content

Conversation

@Kha
Copy link
Member

@Kha Kha commented Oct 16, 2025

This PR improves the error message of generalized field notation if the issue is that the resolved declaration is not visible in the current context.

@Kha Kha added the changelog-no Do not include this PR in the release changelog label Oct 16, 2025
@Kha Kha force-pushed the push-mvktrrroqrvt branch from 5be3b85 to ba1be2c Compare October 16, 2025 10:37
@Kha Kha enabled auto-merge October 16, 2025 10:37
@Kha Kha force-pushed the push-mvktrrroqrvt branch 2 times, most recently from 1bb0f3b to 5dd1254 Compare October 17, 2025 08:22
@Kha Kha force-pushed the push-mvktrrroqrvt branch from 5dd1254 to 673868d Compare October 17, 2025 09:18
@Kha Kha added this pull request to the merge queue Oct 17, 2025
Merged via the queue into leanprover:master with commit 69d8d63 Oct 17, 2025
14 checks passed
@Kha Kha deleted the push-mvktrrroqrvt branch October 17, 2025 10:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant