commit: 855586691d740ee5149ddec36c1a9a952620d23a

[log]
author: Kim Morrison <kim@tqft.net>

Tue Jan 27 01:21:47 2026 +0000
committer: Kim Morrison <kim@tqft.net>

Tue Jan 27 01:23:42 2026 +0000
tree: 0ac8150aef61f38c7bf724708295962a7d113957
parent: 642863e8c5befe8db0b61bbf2f5c9da57c66a45b [diff]

fix: correct comment about instance implicit arguments

This PR fixes a comment that said "implicit arguments" when the code
actually checks `isInstImplicit`, which is specifically for instance
implicit arguments (`[...]` binders), not all implicit arguments.

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

Co-Authored-By: Claude <noreply@anthropic.com>

src/Lean/LibrarySuggestions/Basic.lean[diff]

1 file changed

tree: 0ac8150aef61f38c7bf724708295962a7d113957

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.