#where command #
The #where command prints information about the current location, including the namespace,
active open, universe, and variable commands, and any options set with set_option.
#where gives a description of the global scope at this point in the module.
This includes the namespace, open namespaces, universe and variable commands,
and options set with set_option.
Equations
- Batteries.Tactic.Where.«command#where» = Lean.ParserDescr.node `Batteries.Tactic.Where.command#where 1024 (Lean.ParserDescr.symbol "#where")