# Lean Notes Unused variables Use the underbar prefix convention instead of the linter command. `Example:` ```lean theorem pPQP' : p → q → p := fun (hp : p) (_hq : q) => hp -- (_hq is not used for the proof) ``` The `set_option linter.unusedVariables false` directive can be used for the same effect but the underbar prefix syntax explicitly indicates which terms are actually unused. This is especially useful when a term is used redundantly as in p → q → q → p . ```lean theorem pPPPP : P → P → P → P := -- An example of four duplicates of P. The underbar prefixes in the hypothesis names, adhere to the -- Unused variables coding guideline, . fun (hP _hp _hP' : P) => hP ``` # Variable shadowing Use the underbar prefix convention to indicate that shadowed variables are not only duplications, but that they are unused as well. For instance, when the hP terms is shadowed multiple times, the only term that will be referenced subsequently is hP ```lean theorem pPPPP : P → P → P → P := -- We define the two duplicate terms using the underbar and single quote conventions fun (hP _hp _hP' : P) => hP ```