mathlib3 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.

source
def tactic_doc.command.localized notation  :
tactic_doc_entry

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

  • Declare notation which is localized to a locale using:
localized "infix (name := my_add) ` ⊹ `: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 (name := my_add) ⊹ :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/file:

open_locale my.add
  • More generally, the following will declare all localized notation in the specified locales.
open_locale locale1 locale2 ...
  • You can also declare other localized commands, like local attributes
localized "attribute [simp] le_refl" in le
  • To see all localized commands in a given locale, run:
run_cmd print_localized_commands [`my.add].
  • To see a list of all locales with localized commands, run:
run_cmd do
  m ← localized_attr.get_cache,
  tactic.trace m.keys -- change to `tactic.trace m.to_list` to list all the commands in each locale

  • Warning: You have to give full names of all declarations used in localized notation, so that the localized notation also works when the appropriate namespaces are not opened.

  • Note: In mathlib, you should always provide names for localized notations using the (name := ...) parameter. This prevents issues if the localized notation overrides an existing notation when it gets opened.

  • Warning: Due to limitations in the implementation, you cannot use _ in localized notations. (Otherwise open_locale foo will fail if foo is already opened or partially opened.) Instead, you should use the hole! notation as a drop-in replacement. For example:

-- BAD
-- localized "infix (name := my_add) ` ⊹[` R `] ` := my_add _ R" in foo
-- GOOD
localized "infix (name := my_add) ` ⊹[` R `] ` := my_add hole! R" in foo