mathlib documentation

tactic.localized

Localized notation

This consists of two user-commands which allow you to declare notation and commands localized to a locale.

See the tactic doc entry below for more information.

The code is inspired by code from Gabriel Ebner from the hott3 repository.

source
meta def localized_attr  :
(user_attribute (native.rb_lmap name string))

source
meta def get_localized (ns : list name) :
tactic (list string)

Get all commands in the given locale and return them as a list of strings

source
meta def open_locale_cmd (_x : interactive.parse (lean.parser.tk "open_locale")) :
lean.parser unit

Execute all commands in the given locale

source
meta def localized_cmd (_x : interactive.parse (lean.parser.tk "localized")) :
lean.parser unit

Add a new command to a locale and execute it right now. The new command is added as a declaration to the environment with name _localized_decl.<number>. This declaration has attribute _localized and as value a name-string pair.