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.

meta def where.binder_priority  :

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

The relation on binder priorities.

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
• (a :: rest) = where.select_for_which._match_2 p b' a rest)
• = (list.nil γ, list.nil α)
• where.select_for_which._match_2 p b' a (cs, others) = where.select_for_which._match_1 b' a cs others (p a)
• where.select_for_which._match_1 b' a cs others (b, c) = ite (b = b') (c :: cs, others) (cs, a :: others)
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.

meta def where.sort_variable_list (l : list ) :

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

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

meta def where.format_variable  :

Format an individual variable definition for printing.

meta def where.compile_variable_list (l : list ) :

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

meta def where.get_open_namespaces (ns : 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).

meta def where.build_str_namespace (ns : name) :

#where output helper which traces the current namespace.

#where output helper which traces the open namespaces.

#where output helper which traces the variables.

#where output helper which traces the includes.

meta def where.build_str_end (ns : name) :

#where output helper which traces the namespace end.

meta def where.build_msg  :

#where output main function.

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

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.