mathlib documentation

tactic.localized

Localized notation

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

meta def get_localized  :

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

Execute all commands in the given notation namespace

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.