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>
2026-03-22 04:44:07 +00:00 · 2026-01-27 01:23:42 +00:00
1 changed files with 1 additions and 1 deletions
--- a/src/Lean/LibrarySuggestions/Basic.lean
+++ b/src/Lean/LibrarySuggestions/Basic.lean
@@ -66,7 +66,7 @@ unsafe def fold {α : Type} (f : Name → α → MetaM α) (e : Expr) (acc : α)
    | .app f a           =>
      let fi ← getFunInfo f (some 1)
      if fi.paramInfo[0]!.isInstImplicit then
-        -- Don't visit implicit arguments.
+        -- Don't visit instance implicit arguments.
        visit f acc
      else
        visit a (← visit f acc)