Commit 2019-09-03 18:22 b5b40c74

chore(*): use localized command in mathlib (#1319)

• chore(*): use localized command in mathlib remove some open_locale instances in files that do not import tactic.basic fix some errors type class inference failure fix some more errors typo fully specify all names in localized notation also add some comments to the doc one more localized import checkpoint there is something seriously wrong with type class inference + the transition from constructive to classical logic. Suppose you want to work purely classically, and state a lemma where the statement requires a proof of decidable equality on one of the types. For an abstract type, the only instance of this is classical.prop_decidable, unless you add explicitly an argument that the respective type has decidable equality (which you tend to not want to do if you only work classically). Now when you apply this lemma to a concrete type, where we can infer decidability of equality, type class inference will complain that we used the wrong instance (which is kinda insane: by unification it knows exactly which instance we want to use). A big problem with this, is that you have no idea you will run into this issues later when stating the lemma: Lean will happily accept it
• add TODOs
• fix some errors
• update .gitignore
• fix some timeouts
• replace a couple more local notations