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
: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 leThe code is inspired by code from Gabriel Ebner from the hott3 repository.
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
This declaration has attribute
_localized and as value a name-string pair.