chore(library/init): avoid local attribute

library/init/control/monad.lean

@@ -27,9 +27,8 @@ class Monad (m : Type u → Type v) extends Applicative m, HasBind m : Type (max
 (seqLeft  := λ α β x y, x >>= λ a, y >>= λ _, pure a)
 (seqRight := λ α β x y, x >>= λ _, y)
 
+instance monadInhabited' {α : Type u} {m : Type u → Type v} [Monad m] : Inhabited (α → m α) :=
+⟨pure⟩
+
 instance monadInhabited {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) :=
 ⟨pure $ default _⟩
-
-/- Alternative instance -/
-def monadInhabited' {α : Type u} {m : Type u → Type v} [Monad m] : Inhabited (α → m α) :=
-⟨pure⟩

library/init/core.lean

@@ -1754,11 +1754,9 @@ noncomputable def propDecidable (a : Prop) : Decidable a :=
 choice $ Or.elim (em a)
   (assume ha, ⟨isTrue ha⟩)
   (assume hna, ⟨isFalse hna⟩)
-local attribute [instance] propDecidable
 
 noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) :=
 ⟨propDecidable a⟩
-local attribute [instance] decidableInhabited
 
 noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α :=
 {decEq := λ x y, propDecidable (x = y)}
@@ -1770,10 +1768,12 @@ match (propDecidable (Nonempty α)) with
 
 noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop)
   (h : Nonempty α) : {x : α // Exists (λ y : α, p y) → p x} :=
-if hp : Exists (λ x : α, p x) then
-  let xp := indefiniteDescription _ hp in
-  ⟨xp.val, λ h', xp.property⟩
-else ⟨choice h, λ h, absurd h hp⟩
+@dite (Exists (λ x : α, p x)) (propDecidable _) _
+  (λ hp : Exists (λ x : α, p x),
+    show {x : α // Exists (λ y : α, p y) → p x}, from
+    let xp := indefiniteDescription _ hp in
+    ⟨xp.val, λ h', xp.property⟩)
+  (λ hp, ⟨choice h, λ h, absurd h hp⟩)
 
 /- the Hilbert epsilon Function -/
 
@@ -1808,10 +1808,10 @@ Or.elim (em a)
 
 -- this supercedes byCases in Decidable
 theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q :=
-Decidable.byCases hpq hnpq
+@Decidable.byCases _ _ (propDecidable _) hpq hnpq
 
 -- this supercedes byContradiction in Decidable
 theorem byContradiction {p : Prop} (h : ¬p → False) : p :=
-Decidable.byContradiction h
+@Decidable.byContradiction _ (propDecidable _) h
 
 end Classical

library/init/data/array/basic.lean

@@ -137,7 +137,6 @@ partial def shrink : Array α → Nat → Array α
 
 section
 variables {m : Type v → Type v} [Monad m]
-local attribute [instance] monadInhabited'
 
 -- TODO(Leo): justify termination using wf-rec
 @[specialize] partial def miterateAux (a : Array α) (f : Π i : Fin a.size, α → β → m β) : Nat → β → m β

library/init/data/persistentarray/basic.lean

@@ -127,7 +127,6 @@ else
 
 section
 variables {m : Type v → Type v} [Monad m]
-local attribute [instance] monadInhabited'
 
 @[specialize] partial def mfoldlAux (f : β → α → m β) : PersistentArrayNode α → β → m β
 | (node cs) b := cs.mfoldl (λ b c, mfoldlAux c b) b

library/init/lean/syntax.lean

@@ -105,8 +105,6 @@ match s with
 | Syntax.node kind args scopes := fn ⟨Syntax.node kind (args.map (flipScopes scopes)) [], IsNode.mk _ _ _⟩
 | other                        := base
 
-local attribute [instance] monadInhabited
-
 @[specialize] partial def mreplace {m : Type → Type} [Monad m] (fn : Syntax → m (Option Syntax)) : Syntax → m Syntax
 | stx@(node kind args scopes) := do
   o ← fn stx,

library/init/lean/trace.lean

@@ -33,10 +33,9 @@ structure TraceState :=
 (curPos : Option Position)
 (curTraces : List Trace)
 
-def TraceT (m : Type → Type u) := StateT TraceState m
-local attribute [reducible] TraceT
+abbrev TraceT (m : Type → Type u) := StateT TraceState m
 
-instance (m) [Monad m] : Monad (TraceT m) := inferInstance
+instance (m) [Monad m] : Monad (TraceT m) := inferInstanceAs (Monad (StateT TraceState m))
 
 class MonadTracer (m : Type → Type u) :=
 (traceRoot {α} : Position → Name → Message → Thunk (m α) → m α)

src/frontends/lean/builtin_cmds.cpp

@@ -286,15 +286,6 @@ environment open_export_cmd(parser & p, bool open) {
 static environment open_cmd(parser & p) { return open_export_cmd(p, true); }
 static environment export_cmd(parser & p) { return open_export_cmd(p, false); }
 
-static environment local_cmd(parser & p) {
-    if (p.curr_is_token_or_id(get_attribute_tk())) {
-        p.next();
-        return local_attribute_cmd(p);
-    } else {
-        throw exception("invalid 'local' command, 'attribute' expected");
-    }
-}
-
 static environment help_cmd(parser & p) {
     auto rep = p.mk_message(p.cmd_pos(), INFORMATION);
     if (p.curr_is_token_or_id(get_options_tk())) {
@@ -494,7 +485,6 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("namespace",         "open a new namespace", namespace_cmd));
     add_cmd(r, cmd_info("end",               "close the current namespace/section", end_scoped_cmd));
     add_cmd(r, cmd_info("#check",            "type check given expression, and display its type", check_cmd));
-    add_cmd(r, cmd_info("local",             "define local attributes or notation", local_cmd));
     add_cmd(r, cmd_info("#help",             "brief description of available commands and options", help_cmd));
     add_cmd(r, cmd_info("initQuot",          "initialize `quot` type computational rules", init_quot_cmd));
     add_cmd(r, cmd_info("import",            "import module(s)", import_cmd));