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

feat(tactic/localized): localized notation #1081

mergify merged 15 commits into master from localized_notation

fpvandoorn added WIP

fpvandoorn added RFC

fpvandoorn requested a review 7 years ago

fpvandoorn removed WIP

robertylewis changed the title ~~Localized notation~~ feat(tactic/localized): localized notation 6 years ago

avigad commented on 2019-06-27

fpvandoorn force pushed from 63c6b5e2 to a6fef3c6 6 years ago

fpvandoorn force pushed from 5deaf93a to 4f1a3ac8 6 years ago

robertylewis assigned

robertylewis 6 years ago

fpvandoorn force pushed from 884e2603 to 17f14584 6 years ago

robertylewis approved these changes on 2019-07-11

fpvandoorn force pushed from 286c1ef2 to e6c70b65 6 years ago

first prototype of localized notation

66e82680

update

58b4659d

add test file

7c172b52

shorten command, fix test

a7f1c866

update documentation

1a1d717f

rename files, add to tactic/default

bc5c279d

typo

f2eb9a20

mention that we can use other commands

d6eb2548

optimize

25d8c9aa

only use 1 attribute

fce0740d

add localized command classical instance

104c0c33

use rb_lmap

58b991f4

move rb_lmap.of_list to correct file

0a20014f

rename open_notation to open_locale

519d4092

fpvandoorn force pushed from e6c70b65 to 519d4092 6 years ago

robertylewis removed RFC

robertylewis added ready-to-merge

Merge branch 'master' into localized_notation

7551469c

mergify merged 2511faf4 into master 6 years ago

mergify deleted the localized_notation branch 6 years ago

Reviewers

robertylewis

avigad

Assignees

robertylewis

Labels

ready-to-merge

Milestone

No milestone

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

feat(tactic/localized): localized notation #1081

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

Merged