Commit 2026-03-25 12:45 b71b8d3f

chore(Tactic/Recall): suppress unused variable linter (#37143) This PR suppresses the unused variable linter within the recall command elaborator. Since recall doesn't introduce new definitions (it only checks type-correctness against existing ones), unused variable warnings on binders that appear only in the type are noise. For example, recall Eq.symm {α : Sort _} {a b : α} (h : a = b) : b = a would previously warn about h being unused. 🤖 Prepared with Claude Code