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

def Std.Tactic.Where.«command#where» : Lean.ParserDescr

#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

• Std.Tactic.Where.«command#where» = Lean.ParserDescr.node `Std.Tactic.Where.command#where 1024 (Lean.ParserDescr.symbol "#where")