Skip to content

Conversation

@alok
Copy link
Contributor

@alok alok commented Dec 30, 2025

This PR uses backticks instead of single quotes for identifiers in core messages and tests, following Lean's convention for referring to identifiers in error messages and documentation.

🤖 Generated with Claude Code

@alok alok marked this pull request as ready for review January 1, 2026 22:22
alok and others added 2 commits January 12, 2026 00:36
Update test expectations to match the new backtick formatting for
identifiers in diagnostic messages.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <[email protected]>
@alok alok force-pushed the backticks-core-tests branch from f998a55 to 7cd1b03 Compare January 12, 2026 08:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant