Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-11 18:24 2511faf4

View on Github →

feat(tactic/localized): localized notation (#1081)

  • first prototype of localized notation
  • update
  • add test file
  • shorten command, fix test
  • update documentation
  • rename files, add to tactic/default
  • typo
  • mention that we can use other commands
  • optimize
  • only use 1 attribute
  • add localized command classical instance
  • use rb_lmap This changes the internal code to avoid import clashes and adds a test to that effect
  • move rb_lmap.of_list to correct file also update docstring
  • rename open_notation to open_locale

Estimated changes