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.

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 notation namespace 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 notation namespace

source

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

lean.parser unit

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.

source

meta def print_localized_commands (ns : list name) :

tactic unit

Print all commands in a given notation namespace