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.
#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.