mathlib documentation

tactic.where

The where command #

When working in a Lean file with namespaces, parameters, and variables, it can be confusing to identify what the current "parser context" is. The command #where identifies and prints information about the current location, including the active namespace, open namespaces, and declared variables.

It is a bug for #where to incorrectly report this information (this was not formerly the case); please file an issue on GitHub if you observe a failure.

source
meta def where.binder_priority  :
binder_info → ℕ

Assigns a priority to each binder for determining the order in which variables are traced.

source
meta def where.binder_less_important (u v : binder_info) :
bool

The relation on binder priorities.

source
def where.select_for_which {α β γ : Type} (p : α → β × γ) [decidable_eq β] (b' : β) :
list α → list γ × list α

Selects the elements of the given list α which under the image of p : α → β × γ have β component equal to b'. Returns the γ components of the selected elements under the image of p, and the elements of the original list α which were not selected.

Equations
source
meta def where.collect_by {α β γ : Type} (l : list α) (p : α → β × γ) [decidable_eq β] :
list (β × list γ)

Returns the elements of l under the image of p, collecting together elements with the same β component, deleting duplicates.

source
meta def where.sort_variable_list (l : list (name × binder_info × expr)) :
list (expr × binder_info × list name)

Sort the variables by their priority as defined by where.binder_priority.

source
meta def where.collect_implicit_names  :
list name → list string × list string

Separate out the names of implicit variables (commonly instances with no name).

source
meta def where.format_variable  :
expr × binder_info × list name → tactic string

Format an individual variable definition for printing.

source
meta def where.compile_variable_list (l : list (name × binder_info × expr)) :
tactic string

Turn a list of triples of variable names, binder info, and types, into a pretty list.

source
meta def where.get_open_namespaces (ns : name) :
tactic (list name)

get_open_namespaces ns returns a list of the open namespaces, given that we are currently in the namespace ns (which we do not include).

source
meta def where.build_str_namespace (ns : name) :
lean.parser string

#where output helper which traces the current namespace.

source
meta def where.build_str_open_namespaces (ns : name) :
tactic string

#where output helper which traces the open namespaces.

source
meta def where.build_str_variables  :
lean.parser string

#where output helper which traces the variables.

source
meta def where.build_str_includes  :
lean.parser string

#where output helper which traces the includes.

source
meta def where.build_str_end (ns : name) :
tactic string

#where output helper which traces the namespace end.

source
meta def where.build_msg  :
lean.parser string

#where output main function.

source
meta def where.where_cmd (_x : interactive.parse (lean.parser.tk "#where")) :
lean.parser unit

When working in a Lean file with namespaces, parameters, and variables, it can be confusing to identify what the current "parser context" is. The command #where identifies and prints information about the current location, including the active namespace, open namespaces, and declared variables.

It is a bug for #where to incorrectly report this information (this was not formerly the case); please file an issue on GitHub if you observe a failure.