Code

Add unused variables linter#1159

Code

Merged

Kha merged 11 commits intoleanprover:masterleanprover/lean4:masterfrom larsk21:linter/unused-variableslarsk21/lean4:linter/unused-variablesCopy head branch name to clipboardJun 3, 2022

+536-38

Commits

Commits on Jun 3, 2022

• fix: run linters after elaboration

  

  larsk21

  authored and

  Kha

  committed
  f092843

  Copy full SHA for f092843

• fix: add additional information to Lean.Server.Reference

  

  larsk21

  authored and

  Kha

  committed
  60a66e8

  Copy full SHA for 60a66e8

• feat: add unused variables linter

  

  larsk21

  authored and

  Kha

  committed
  765bb7d

  Copy full SHA for 765bb7d

• fix: disable linters in tests

  

  larsk21

  authored and

  Kha

  committed
  ce3f83a

  Copy full SHA for ce3f83a

• fix: forward lean options to workers

  

  larsk21

  authored and

  Kha

  committed
  4519a7c

  Copy full SHA for 4519a7c

• fix: unused variables linter review comments

  Show description for e92df38
  

  larsk21

  authored and

  Kha

  committed
  e92df38

  Copy full SHA for e92df38

• refactor: extend Lsp.ModuleRefs in Server.References

  

  larsk21

  authored and

  Kha

  committed
  f56b1d3

  Copy full SHA for f56b1d3

• fix: use findModuleRefs in unused variables linter

  

  larsk21

  authored and

  Kha

  committed
  8d3e80c

  Copy full SHA for 8d3e80c

• fix: ignore exposed function arguments in unused variables linter

  

  larsk21

  authored and

  Kha

  committed
  11fe65a

  Copy full SHA for 11fe65a

• fix: consider tactic mvar assignments for used variables

  

  larsk21

  authored and

  Kha

  committed
  c1fab4d

  Copy full SHA for c1fab4d

• feat: add nolint options for function arguments and pattern variables

  

  larsk21

  authored and

  Kha

  committed
  301e8fb

  Copy full SHA for 301e8fb