The #show_unused command

#show_unused decl1 decl2 .. will highlight every theorem or definition in the current file not involved in the definition of declarations decl1, decl2, etc. The result is shown both in the message on #show_unused, as well as on the declarations themselves.

def Batteries.Tactic.ShowUnused.«command#show_unused___» : Lean.ParserDescr

#show_unused decl1 decl2 .. will highlight every theorem or definition in the current file not involved in the definition of declarations decl1, decl2, etc. The result is shown both in the message on #show_unused, as well as on the declarations themselves.

def foo := 1
def baz := 2
def bar := foo
#show_unused bar -- highlights `baz`

Equations

• One or more equations did not get rendered due to their size.