tactic.localized

# Localized notation

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

• Declare notation which is localized to a namespace using: lean localized "infix  ⊹ :60 := my_add" in my.add 
• After this command it will be available in the same section/namespace/file, just as if you wrote local infix:60 := my_add
• You can open it in other places. The following command will declare the notation again as local notation in that section/namespace/files: lean open_locale my.add 
• More generally, the following will declare all localized notation in the specified namespaces. lean open_locale namespace1 namespace2 ... 
• You can also declare other localized commands, like local attributes lean localized "attribute [simp] le_refl" in le  The code is inspired by code from Gabriel Ebner from the hott3 repository.
meta def localized_attr  :

meta def get_localized  :

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

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

Execute all commands in the given notation namespace

meta def localized_cmd  :

Add a new command to a notation namespace 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.