From 33a10130cfbc9fff73033666c4af3ac64ed74a37 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 12 May 2020 14:27:49 -0700
Subject: [PATCH] chore: fix stdlib

---
 src/Init/Control/Alternative.lean          |  3 +-
 src/Init/Control/Applicative.lean          |  2 +-
 src/Init/Control/EState.lean               |  4 +--
 src/Init/Control/Except.lean               | 10 +++---
 src/Init/Control/Lift.lean                 |  8 ++---
 src/Init/Control/Reader.lean               |  6 ++--
 src/Init/Control/State.lean                | 10 +++---
 src/Init/Core.lean                         | 40 +++++++++++-----------
 src/Init/Data/AssocList.lean               |  2 +-
 src/Init/Data/BinomialHeap/Basic.lean      |  6 ++--
 src/Init/Data/PersistentHashMap/Basic.lean |  6 ++--
 src/Init/Data/RBMap/Basic.lean             |  4 +--
 src/Init/Lean/Data/Json/FromToJson.lean    |  2 +-
 src/Init/Lean/Data/Json/Parser.lean        |  8 ++---
 src/Init/Lean/Data/KVMap.lean              |  6 ++--
 src/Init/Lean/Data/LOption.lean            |  6 ++--
 src/Init/Lean/Elab/Log.lean                | 10 +++---
 src/Init/Lean/Elab/StructInst.lean         |  6 ++--
 src/Init/Lean/Elab/Util.lean               | 12 +++----
 src/Init/Lean/Util/MonadCache.lean         |  8 ++---
 src/Init/Lean/Util/Trace.lean              | 22 ++++++------
 src/Init/LeanInit.lean                     | 10 +++---
 src/Init/ShareCommon.lean                  |  2 +-
 src/Init/Util.lean                         |  2 +-
 src/Init/WF.lean                           |  8 ++---
 25 files changed, 101 insertions(+), 102 deletions(-)

diff --git a/src/Init/Control/Alternative.lean b/src/Init/Control/Alternative.lean
index 6b5754dfb8..0f6081a680 100644
--- a/src/Init/Control/Alternative.lean
+++ b/src/Init/Control/Alternative.lean
@@ -18,8 +18,7 @@ instance alternativeHasOrelse (f : Type u → Type v) (α : Type u) [Alternative
 section
 variables {f : Type u → Type v} [Alternative f] {α : Type u}
 
-@[inline] def failure : f α :=
-Alternative.failure f
+export Alternative (failure)
 
 @[inline] def guard {f : Type → Type v} [Alternative f] (p : Prop) [Decidable p] : f Unit :=
 if p then pure () else failure
diff --git a/src/Init/Control/Applicative.lean b/src/Init/Control/Applicative.lean
index 8e80b9c5c9..28dd82a56d 100644
--- a/src/Init/Control/Applicative.lean
+++ b/src/Init/Control/Applicative.lean
@@ -9,7 +9,7 @@ open Function
 universes u v
 
 class HasPure (f : Type u → Type v) :=
-(pure {} {α : Type u} : α → f α)
+(pure {α : Type u} : α → f α)
 
 export HasPure (pure)
 
diff --git a/src/Init/Control/EState.lean b/src/Init/Control/EState.lean
index bab6287d07..63a54be6ef 100644
--- a/src/Init/Control/EState.lean
+++ b/src/Init/Control/EState.lean
@@ -11,8 +11,8 @@ universes u v
 namespace EStateM
 
 inductive Result (ε σ α : Type u)
-| ok    {} : α → σ → Result
-| error {} : ε → σ → Result
+| ok    : α → σ → Result
+| error : ε → σ → Result
 
 variables {ε σ α : Type u}
 
diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index 8cd89a207e..f0a607f9e6 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -12,8 +12,8 @@ import Init.Data.ToString
 universes u v w
 
 inductive Except (ε : Type u) (α : Type v)
-| error {} : ε → Except
-| ok {} : α → Except
+| error : ε → Except
+| ok    : α → Except
 
 attribute [unbox] Except
 
@@ -127,8 +127,8 @@ end ExceptT
 
 /-- An implementation of [MonadError](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Except.html#t:MonadError) -/
 class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) :=
-(throw {} {α : Type v} : ε → m α)
-(catch {} {α : Type v} : m α → (ε → m α) → m α)
+(throw {α : Type v} : ε → m α)
+(catch {α : Type v} : m α → (ε → m α) → m α)
 
 namespace MonadExcept
 variables {ε : Type u} {m : Type v → Type w}
@@ -164,7 +164,7 @@ instance (ε) : MonadExcept ε (Except ε) :=
     ```
 -/
 class MonadExceptAdapter (ε ε' : outParam (Type u)) (m m' : Type u → Type v) :=
-(adaptExcept {} {α : Type u} : (ε → ε') → m α → m' α)
+(adaptExcept {α : Type u} : (ε → ε') → m α → m' α)
 export MonadExceptAdapter (adaptExcept)
 
 section
diff --git a/src/Init/Control/Lift.lean b/src/Init/Control/Lift.lean
index 1b7549edbb..0f056a4dd4 100644
--- a/src/Init/Control/Lift.lean
+++ b/src/Init/Control/Lift.lean
@@ -19,13 +19,13 @@ universes u v w
     but `n` does not have to be a monad transformer.
     Alternatively, an implementation of [MonadLayer](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLayer) without `layerInvmap` (so far). -/
 class HasMonadLift (m : Type u → Type v) (n : Type u → Type w) :=
-(monadLift {} : ∀ {α}, m α → n α)
+(monadLift : ∀ {α}, m α → n α)
 
 /-- The reflexive-transitive closure of `HasMonadLift`.
     `monadLift` is used to transitively lift monadic computations such as `StateT.get` or `StateT.put s`.
     Corresponds to [MonadLift](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLift). -/
 class HasMonadLiftT (m : Type u → Type v) (n : Type u → Type w) :=
-(monadLift {} : ∀ {α}, m α → n α)
+(monadLift : ∀ {α}, m α → n α)
 
 export HasMonadLiftT (monadLift)
 
@@ -53,13 +53,13 @@ theorem monadLiftRefl {m : Type u → Type v} {α} : (monadLift : m α → m α)
     Remark: other libraries equate `m` and `m'`, and `n` and `n'`. We need to distinguish them to be able to implement
     gadgets such as `MonadStateAdapter` and `MonadReaderAdapter`. -/
 class MonadFunctor (m m' : Type u → Type v) (n n' : Type u → Type w) :=
-(monadMap {} {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α)
+(monadMap {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α)
 
 /-- The reflexive-transitive closure of `MonadFunctor`.
     `monadMap` is used to transitively lift Monad morphisms such as `StateT.zoom`.
     A generalization of [MonadLiftFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadLiftFunctor), which can only lift endomorphisms (i.e. m = m', n = n'). -/
 class MonadFunctorT (m m' : Type u → Type v) (n n' : Type u → Type w) :=
-(monadMap {} {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α)
+(monadMap {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α)
 
 export MonadFunctorT (monadMap)
 
diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean
index 68f2fbac68..cdb4717e63 100644
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@@ -81,7 +81,7 @@ end ReaderT
     ```
     -/
 class MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) :=
-(read {} : m ρ)
+(read : m ρ)
 
 export MonadReader (read)
 
@@ -104,7 +104,7 @@ instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadReader ρ (Reade
     ```
     -/
 class MonadReaderAdapter (ρ ρ' : outParam (Type u)) (m m' : Type u → Type v) :=
-(adaptReader {} {α : Type u} : (ρ' → ρ) → m α → m' α)
+(adaptReader {α : Type u} : (ρ' → ρ) → m α → m' α)
 export MonadReaderAdapter (adaptReader)
 
 section
@@ -121,7 +121,7 @@ instance (ρ : Type u) (m out) [MonadRun out m] : MonadRun (fun α => ρ → out
 ⟨fun α x => run ∘ x⟩
 
 class MonadReaderRunner (ρ : Type u) (m m' : Type u → Type u) :=
-(runReader {} {α : Type u} : m α → ρ → m' α)
+(runReader {α : Type u} : m α → ρ → m' α)
 export MonadReaderRunner (runReader)
 
 section
diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean
index 0e60bb45d0..77a8cb96e0 100644
--- a/src/Init/Control/State.lean
+++ b/src/Init/Control/State.lean
@@ -91,14 +91,14 @@ end StateT
     automatically from `monadLift`. -/
 class MonadState (σ : outParam (Type u)) (m : Type u → Type v) :=
 /- Obtain the top-most State of a Monad stack. -/
-(get {} : m σ)
+(get : m σ)
 /- Set the top-most State of a Monad stack. -/
-(set {} : σ → m PUnit)
+(set : σ → m PUnit)
 /- Map the top-most State of a Monad stack.
 
    Note: `modifyGet f` may be preferable to `do s <- get; let (a, s) := f s; put s; pure a`
    because the latter does not use the State linearly (without sufficient inlining). -/
-(modifyGet {} {α : Type u} : (σ → α × σ) → m α)
+(modifyGet {α : Type u} : (σ → α × σ) → m α)
 
 export MonadState (get set modifyGet)
 
@@ -159,7 +159,7 @@ end
     ```
     -/
 class MonadStateAdapter (σ σ' : outParam (Type u)) (m m' : Type u → Type v) :=
-(adaptState {} {σ'' α : Type u} (split : σ' → σ × σ'') (join : σ → σ'' → σ') : m α → m' α)
+(adaptState {σ'' α : Type u} (split : σ' → σ × σ'') (join : σ → σ'' → σ') : m α → m' α)
 export MonadStateAdapter (adaptState)
 
 section
@@ -180,7 +180,7 @@ instance (σ : Type u) (m out : Type u → Type v) [MonadRun out m] [Functor m]
 ⟨fun α x => run ∘ StateT.run' x⟩
 
 class MonadStateRunner (σ : Type u) (m m' : Type u → Type u) :=
-(runState {} {α : Type u} : m α → σ → m' α)
+(runState {α : Type u} : m α → σ → m' α)
 export MonadStateRunner (runState)
 
 section
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index b29f991284..bdade2ccdf 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -180,7 +180,7 @@ def Not (a : Prop) : Prop := a → False
 prefix `¬` := Not
 
 inductive Eq {α : Sort u} (a : α) : α → Prop
-| refl : Eq a
+| refl {} : Eq a
 
 @[elabAsEliminator, inline, reducible]
 def Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : α → Sort u1} (m : C a) {b : α} (h : Eq a b) : C b :=
@@ -206,7 +206,7 @@ constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop}
 init_quot
 
 inductive HEq {α : Sort u} (a : α) : ∀ {β : Sort u}, β → Prop
-| refl : HEq a
+| refl {} : HEq a
 
 structure Prod (α : Type u) (β : Type v) :=
 (fst : α) (snd : β)
@@ -254,16 +254,16 @@ show (Eq.ndrecOn (Eq.refl α) a : α) = a' from
   this α a' h (Eq.refl α)
 
 inductive Sum (α : Type u) (β : Type v)
-| inl {} (val : α) : Sum
-| inr {} (val : β) : Sum
+| inl (val : α) : Sum
+| inr (val : β) : Sum
 
 inductive PSum (α : Sort u) (β : Sort v)
-| inl {} (val : α) : PSum
-| inr {} (val : β) : PSum
+| inl (val : α) : PSum
+| inr (val : β) : PSum
 
 inductive Or (a b : Prop) : Prop
-| inl {} (h : a) : Or
-| inr {} (h : b) : Or
+| inl (h : a) : Or
+| inr (h : b) : Or
 
 def Or.introLeft {a : Prop} (b : Prop) (ha : a) : Or a b :=
 Or.inl ha
@@ -307,7 +307,7 @@ def decEq {α : Sort u} [s : DecidableEq α] (a b : α) : Decidable (a = b) :=
 s a b
 
 inductive Option (α : Type u)
-| none {} : Option
+| none : Option
 | some (val : α) : Option
 
 attribute [unbox] Option
@@ -316,7 +316,7 @@ export Option (none some)
 export Bool (false true)
 
 inductive List (T : Type u)
-| nil {} : List
+| nil : List
 | cons (hd : T) (tl : List) : List
 
 infixr `::` := List.cons
@@ -332,8 +332,8 @@ axiom sorryAx (α : Sort u) (synthetic := true) : α
 
 /- Declare builtin and reserved notation -/
 
-class HasZero     (α : Type u) := (zero : α)
-class HasOne      (α : Type u) := (one : α)
+class HasZero     (α : Type u) := mk {} :: (zero : α)
+class HasOne      (α : Type u) := mk {} :: (one : α)
 class HasAdd      (α : Type u) := (add : α → α → α)
 class HasMul      (α : Type u) := (mul : α → α → α)
 class HasNeg      (α : Type u) := (neg : α → α)
@@ -365,7 +365,7 @@ infix `≤`        := HasLessEq.LessEq
 infix `<`        := HasLess.Less
 infix `==`       := HasBeq.beq
 infix `++`       := HasAppend.append
-notation `∅`   := HasEmptyc.emptyc _
+notation `∅`     := HasEmptyc.emptyc
 infix `≈`        := HasEquiv.Equiv
 infixr `^`       := HasPow.pow
 infixr `/\`      := And
@@ -446,7 +446,7 @@ inductive PNonScalar : Type u
 
 /- For numeric literals notation -/
 class HasOfNat (α : Type u) :=
-(ofNat : Nat → α)
+mk {} :: (ofNat : Nat → α)
 
 export HasOfNat (ofNat)
 
@@ -1080,7 +1080,7 @@ structure PointedType :=
 /- Inhabited -/
 
 class Inhabited (α : Sort u) :=
-(default : α)
+mk {} :: (default : α)
 
 constant arbitrary (α : Sort u) [Inhabited α] : α :=
 Inhabited.default α
@@ -1353,7 +1353,7 @@ fun a b => isTrue (punitEq a b)
 /- Setoid -/
 
 class Setoid (α : Sort u) :=
-(r : α → α → Prop) (iseqv : Equivalence r)
+mk {} :: (r : α → α → Prop) (iseqv : Equivalence r)
 
 instance setoidHasEquiv {α : Sort u} [Setoid α] : HasEquiv α :=
 ⟨Setoid.r⟩
@@ -1600,10 +1600,10 @@ variable {α : Type u}
 variable (r : α → α → Prop)
 
 inductive EqvGen : α → α → Prop
-| rel {} : ∀ x y, r x y → EqvGen x y
-| refl {} : ∀ x, EqvGen x x
-| symm {} : ∀ x y, EqvGen x y → EqvGen y x
-| trans {} : ∀ x y z, EqvGen x y → EqvGen y z → EqvGen x z
+| rel   : ∀ x y, r x y → EqvGen x y
+| refl  : ∀ x, EqvGen x x
+| symm  : ∀ x y, EqvGen x y → EqvGen y x
+| trans : ∀ x y z, EqvGen x y → EqvGen y z → EqvGen x z
 
 theorem EqvGen.isEquivalence : Equivalence (@EqvGen α r) :=
 mkEquivalence _ EqvGen.refl EqvGen.symm EqvGen.trans
diff --git a/src/Init/Data/AssocList.lean b/src/Init/Data/AssocList.lean
index 445da38140..b66edb3ad4 100644
--- a/src/Init/Data/AssocList.lean
+++ b/src/Init/Data/AssocList.lean
@@ -9,7 +9,7 @@ universes u v w
 
 /- List-like type to avoid extra level of indirection -/
 inductive AssocList (α : Type u) (β : Type v)
-| nil {} : AssocList
+| nil : AssocList
 | cons (key : α) (value : β) (tail : AssocList) : AssocList
 
 namespace AssocList
diff --git a/src/Init/Data/BinomialHeap/Basic.lean b/src/Init/Data/BinomialHeap/Basic.lean
index 48f9d9cd08..4a9d8df563 100644
--- a/src/Init/Data/BinomialHeap/Basic.lean
+++ b/src/Init/Data/BinomialHeap/Basic.lean
@@ -13,7 +13,7 @@ structure HeapNodeAux (α : Type u) (h : Type u) :=
 (val : α) (rank : Nat) (children : List h)
 
 inductive Heap (α : Type u) : Type u
-| empty {} : Heap
+| empty     : Heap
 | heap  (ns : List (HeapNodeAux α Heap)) : Heap
 
 abbrev HeapNode (α) := HeapNodeAux α (Heap α)
@@ -94,8 +94,8 @@ partial def toList (lt : α → α → Bool) : Heap α → List α
   | some a => a :: toList (tail lt h)
 
 inductive WellFormed (lt : α → α → Bool) : Heap α → Prop
-| emptyWff                  : WellFormed Heap.empty
-| singletonWff (a : α)      : WellFormed (singleton a)
+| emptyWff {}               : WellFormed Heap.empty
+| singletonWff {} (a : α)   : WellFormed (singleton a)
 | mergeWff (h₁ h₂ : Heap α) : WellFormed h₁ → WellFormed h₂ → WellFormed (merge lt h₁ h₂)
 | tailWff (h : Heap α)      : WellFormed h → WellFormed (tail lt h)
 
diff --git a/src/Init/Data/PersistentHashMap/Basic.lean b/src/Init/Data/PersistentHashMap/Basic.lean
index 0e638f8ac7..d14fb72312 100644
--- a/src/Init/Data/PersistentHashMap/Basic.lean
+++ b/src/Init/Data/PersistentHashMap/Basic.lean
@@ -11,9 +11,9 @@ universes u v w w'
 namespace PersistentHashMap
 
 inductive Entry (α : Type u) (β : Type v) (σ : Type w)
-| entry {} (key : α) (val : β) : Entry
-| ref   {} (node : σ) : Entry
-| null  {} : Entry
+| entry (key : α) (val : β) : Entry
+| ref   (node : σ) : Entry
+| null  : Entry
 
 instance Entry.inhabited {α β σ} : Inhabited (Entry α β σ) := ⟨Entry.null⟩
 
diff --git a/src/Init/Data/RBMap/Basic.lean b/src/Init/Data/RBMap/Basic.lean
index ac3d99dda8..3c21a9a24c 100644
--- a/src/Init/Data/RBMap/Basic.lean
+++ b/src/Init/Data/RBMap/Basic.lean
@@ -13,7 +13,7 @@ inductive Rbcolor
 | red | black
 
 inductive RBNode (α : Type u) (β : α → Type v)
-| leaf  {}                                                                            : RBNode
+| leaf                                                                                : RBNode
 | node  (color : Rbcolor) (lchild : RBNode) (key : α) (val : β key) (rchild : RBNode) : RBNode
 
 namespace RBNode
@@ -199,7 +199,7 @@ variable (lt : α → α → Bool)
 end Membership
 
 inductive WellFormed (lt : α → α → Bool) : RBNode α β → Prop
-| leafWff : WellFormed leaf
+| leafWff {} : WellFormed leaf
 | insertWff {n n' : RBNode α β} {k : α} {v : β k} : WellFormed n → n' = insert lt n k v → WellFormed n'
 | eraseWff {n n' : RBNode α β} {k : α} : WellFormed n → n' = erase lt k n → WellFormed n'
 
diff --git a/src/Init/Lean/Data/Json/FromToJson.lean b/src/Init/Lean/Data/Json/FromToJson.lean
index bc61c0f582..f17f0156fe 100644
--- a/src/Init/Lean/Data/Json/FromToJson.lean
+++ b/src/Init/Lean/Data/Json/FromToJson.lean
@@ -13,7 +13,7 @@ namespace Lean
 universes u
 
 class HasFromJson (α : Type u) :=
-(fromJson? {} : Json → Option α)
+(fromJson? : Json → Option α)
 export HasFromJson (fromJson?)
 
 class HasToJson (α : Type u) :=
diff --git a/src/Init/Lean/Data/Json/Parser.lean b/src/Init/Lean/Data/Json/Parser.lean
index d4967cbd08..5d6545480a 100644
--- a/src/Init/Lean/Data/Json/Parser.lean
+++ b/src/Init/Lean/Data/Json/Parser.lean
@@ -11,8 +11,8 @@ import Init.Control.Except
 namespace Lean
 
 inductive Quickparse.Result (α : Type)
-| success {} (pos : String.Iterator) (res : α) : Quickparse.Result
-| error {} (pos : String.Iterator) (err : String) : Quickparse.Result
+| success (pos : String.Iterator) (res : α) : Quickparse.Result
+| error (pos : String.Iterator) (err : String) : Quickparse.Result
 
 def Quickparse (α : Type) : Type := String.Iterator → Quickparse.Result α
 
@@ -38,7 +38,7 @@ protected def pure {α : Type} (a : α) : Quickparse α | it =>
 success it a
 
 @[inline]
-protected def bind {α β : Type} (f : Quickparse α) (g : α → Quickparse β) : Quickparse β | it => 
+protected def bind {α β : Type} (f : Quickparse α) (g : α → Quickparse β) : Quickparse β | it =>
 match f it with
 | success rem a => g a rem
 | error pos msg => error pos msg
@@ -137,7 +137,7 @@ else do
   ec ←
     if c = '\\' then
       escapedChar
-    -- as to whether c.val > 0xffff should be split up and encoded with multiple \u, 
+    -- as to whether c.val > 0xffff should be split up and encoded with multiple \u,
     -- the JSON standard is not definite: both directly printing the character
     -- and encoding it with multiple \u is allowed. we choose the former.
     else if 0x0020 ≤ c.val ∧ c.val ≤ 0x10ffff then
diff --git a/src/Init/Lean/Data/KVMap.lean b/src/Init/Lean/Data/KVMap.lean
index 283d0be6e4..420135cb79 100644
--- a/src/Init/Lean/Data/KVMap.lean
+++ b/src/Init/Lean/Data/KVMap.lean
@@ -149,9 +149,9 @@ subset m₁ m₂ && subset m₂ m₁
 instance : HasBeq KVMap := ⟨eqv⟩
 
 class isKVMapVal (α : Type) :=
-(defVal : α)
-(set    : KVMap → Name → α → KVMap)
-(get    : KVMap → Name → α → α)
+(defVal {} : α)
+(set       : KVMap → Name → α → KVMap)
+(get       : KVMap → Name → α → α)
 
 export isKVMapVal (set)
 
diff --git a/src/Init/Lean/Data/LOption.lean b/src/Init/Lean/Data/LOption.lean
index ae29a55699..10928e92f6 100644
--- a/src/Init/Lean/Data/LOption.lean
+++ b/src/Init/Lean/Data/LOption.lean
@@ -10,9 +10,9 @@ universes u
 namespace Lean
 
 inductive LOption (α : Type u)
-| none  {} : LOption
-| some     : α → LOption
-| undef {} : LOption
+| none  : LOption
+| some  : α → LOption
+| undef : LOption
 
 namespace LOption
 variables {α : Type u}
diff --git a/src/Init/Lean/Elab/Log.lean b/src/Init/Lean/Elab/Log.lean
index f6cbe1159d..8811ff36e6 100644
--- a/src/Init/Lean/Elab/Log.lean
+++ b/src/Init/Lean/Elab/Log.lean
@@ -11,15 +11,15 @@ namespace Lean
 namespace Elab
 
 class MonadPosInfo (m : Type → Type) :=
-(getFileMap  {} : m FileMap)
-(getFileName {} : m String)
-(getCmdPos   {} : m String.Pos)
-(addContext  {} : MessageData → m MessageData)
+(getFileMap   : m FileMap)
+(getFileName  : m String)
+(getCmdPos    : m String.Pos)
+(addContext   : MessageData → m MessageData)
 
 export MonadPosInfo (getFileMap getFileName getCmdPos)
 
 class MonadLog (m : Type → Type) extends MonadPosInfo m :=
-(logMessage  {} : Message → m Unit)
+(logMessage   : Message → m Unit)
 
 export MonadLog (logMessage)
 
diff --git a/src/Init/Lean/Elab/StructInst.lean b/src/Init/Lean/Elab/StructInst.lean
index 2aed9e89a7..c42953ca4a 100644
--- a/src/Init/Lean/Elab/StructInst.lean
+++ b/src/Init/Lean/Elab/StructInst.lean
@@ -220,9 +220,9 @@ instance FieldLHS.hasFormat : HasFormat FieldLHS :=
   | FieldLHS.modifyOp _ i   => "[" ++ i.prettyPrint ++ "]"⟩
 
 inductive FieldVal (σ : Type)
-| term {} (stx : Syntax) : FieldVal
-| nested (s : σ)         : FieldVal
-| default {}             : FieldVal -- mark that field must be synthesized using default value
+| term  (stx : Syntax) : FieldVal
+| nested (s : σ)       : FieldVal
+| default              : FieldVal -- mark that field must be synthesized using default value
 
 structure Field (σ : Type) :=
 mk {} :: (ref : Syntax) (lhs : List FieldLHS) (val : FieldVal σ) (expr? : Option Expr := none)
diff --git a/src/Init/Lean/Elab/Util.lean b/src/Init/Lean/Elab/Util.lean
index cab1a6f614..c8670e0ffc 100644
--- a/src/Init/Lean/Elab/Util.lean
+++ b/src/Init/Lean/Elab/Util.lean
@@ -106,12 +106,12 @@ fun stx =>
   | none          => throw Macro.Exception.unsupportedSyntax
 
 class MonadMacroAdapter (m : Type → Type) :=
-(getEnv {}                            : m Environment)
-(getCurrMacroScope {}                 : m MacroScope)
-(getNextMacroScope {}                 : m MacroScope)
-(setNextMacroScope {}                 : MacroScope → m Unit)
-(throwError {} {α : Type}             : Syntax → MessageData → m α)
-(throwUnsupportedSyntax {} {α : Type} : m α)
+(getEnv                             : m Environment)
+(getCurrMacroScope                  : m MacroScope)
+(getNextMacroScope                  : m MacroScope)
+(setNextMacroScope                  : MacroScope → m Unit)
+(throwError  {α : Type}             : Syntax → MessageData → m α)
+(throwUnsupportedSyntax  {α : Type} : m α)
 
 @[inline] def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] (x : MacroM α) : m α := do
 scp  ← MonadMacroAdapter.getCurrMacroScope;
diff --git a/src/Init/Lean/Util/MonadCache.lean b/src/Init/Lean/Util/MonadCache.lean
index c44585cc2d..0b5df73ae3 100644
--- a/src/Init/Lean/Util/MonadCache.lean
+++ b/src/Init/Lean/Util/MonadCache.lean
@@ -11,8 +11,8 @@ import Init.Data.HashMap
 namespace Lean
 /-- Interface for caching results.  -/
 class MonadCache (α β : Type) (m : Type → Type) :=
-(findCached? {} : α → m (Option β))
-(cache       {} : α → β → m Unit)
+(findCached? : α → m (Option β))
+(cache       : α → β → m Unit)
 
 /-- If entry `a := b` is already in the cache, then return `b`.
     Otherwise, execute `b ← f a`, store `a := b` in the cache and return `b`. -/
@@ -36,8 +36,8 @@ instance exceptLift {α β ε : Type} {m : Type → Type} [MonadCache α β m] [
 /-- Adapter for implementing `MonadCache` interface using `HashMap`s.
     We just have to specify how to extract/modify the `HashMap`. -/
 class MonadHashMapCacheAdapter (α β : Type) (m : Type → Type) [HasBeq α] [Hashable α] :=
-(getCache {}    : m (HashMap α β))
-(modifyCache {} : (HashMap α β → HashMap α β) → m Unit)
+(getCache    : m (HashMap α β))
+(modifyCache : (HashMap α β → HashMap α β) → m Unit)
 
 namespace MonadHashMapCacheAdapter
 
diff --git a/src/Init/Lean/Util/Trace.lean b/src/Init/Lean/Util/Trace.lean
index a2a5cd6a38..b865252997 100644
--- a/src/Init/Lean/Util/Trace.lean
+++ b/src/Init/Lean/Util/Trace.lean
@@ -11,15 +11,15 @@ namespace Lean
 
 class MonadTracer (m : Type → Type u) :=
 (traceCtx {α} : Name → m α → m α)
-(trace {}  : Name → (Unit → MessageData) → m PUnit)
-(traceM {} : Name → m MessageData → m PUnit)
+(trace  : Name → (Unit → MessageData) → m PUnit)
+(traceM : Name → m MessageData → m PUnit)
 
 class MonadTracerAdapter (m : Type → Type) :=
-(isTracingEnabledFor {} : Name → m Bool)
-(addContext {} : MessageData → m MessageData)
-(enableTracing {} : Bool → m Bool)
-(getTraces {} : m (PersistentArray MessageData))
-(modifyTraces {} : (PersistentArray MessageData → PersistentArray MessageData) → m Unit)
+(isTracingEnabledFor : Name → m Bool)
+(addContext          : MessageData → m MessageData)
+(enableTracing       : Bool → m Bool)
+(getTraces           : m (PersistentArray MessageData))
+(modifyTraces        : (PersistentArray MessageData → PersistentArray MessageData) → m Unit)
 
 private def checkTraceOptionAux (opts : Options) : Name → Bool
 | n@(Name.str p _ _) => opts.getBool n || (!opts.contains n && checkTraceOptionAux p)
@@ -128,10 +128,10 @@ instance : HasToString TraceState := ⟨toString ∘ fmt⟩
 end TraceState
 
 class SimpleMonadTracerAdapter (m : Type → Type) :=
-(getOptions {}       : m Options)
-(modifyTraceState {} : (TraceState → TraceState) → m Unit)
-(getTraceState {}    : m TraceState)
-(addContext {}       : MessageData → m MessageData)
+(getOptions        : m Options)
+(modifyTraceState  : (TraceState → TraceState) → m Unit)
+(getTraceState     : m TraceState)
+(addContext        : MessageData → m MessageData)
 
 namespace SimpleMonadTracerAdapter
 variables {m : Type → Type} [Monad m] [SimpleMonadTracerAdapter m]
diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index 49f55a1d2b..115a600aa8 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -175,10 +175,10 @@ abbrev SyntaxNodeKind := Name
 /- Syntax AST -/
 
 inductive Syntax
-| missing {} : Syntax
+| missing : Syntax
 | node   (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
-| atom   {} (info : Option SourceInfo) (val : String) : Syntax
-| ident  {} (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Name × List String)) : Syntax
+| atom   (info : Option SourceInfo) (val : String) : Syntax
+| ident  (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Name × List String)) : Syntax
 
 instance Syntax.inhabited : Inhabited Syntax :=
 ⟨Syntax.missing⟩
@@ -247,8 +247,8 @@ def firstFrontendMacroScope := reservedMacroScope + 1
     elaboration). -/
 class MonadQuotation (m : Type → Type) :=
 -- Get the fresh scope of the current macro invocation
-(getCurrMacroScope {} : m MacroScope)
-(getMainModule {}     : m Name)
+(getCurrMacroScope : m MacroScope)
+(getMainModule     : m Name)
 /- Execute action in a new macro invocation context. This transformer should be
    used at all places that morally qualify as the beginning of a "macro call",
    e.g. `elabCommand` and `elabTerm` in the case of the elaborator. However, it
diff --git a/src/Init/ShareCommon.lean b/src/Init/ShareCommon.lean
index 7514c93f9b..faca73ca5e 100644
--- a/src/Init/ShareCommon.lean
+++ b/src/Init/ShareCommon.lean
@@ -116,7 +116,7 @@ def PersistentState.shareCommon {α} (s : PersistentState) (a : α) : α × Pers
 end ShareCommon
 
 class MonadShareCommon (m : Type u → Type v) :=
-(withShareCommon {} {α : Type u} : α → m α)
+(withShareCommon {α : Type u} : α → m α)
 
 export MonadShareCommon (withShareCommon)
 
diff --git a/src/Init/Util.lean b/src/Init/Util.lean
index 3584dba211..716c0c0343 100644
--- a/src/Init/Util.lean
+++ b/src/Init/Util.lean
@@ -49,7 +49,7 @@ k (ptrAddrUnsafe a)
 if ptrAddrUnsafe a == ptrAddrUnsafe b then true else k ()
 
 inductive PtrEqResult {α : Type u} (x y : α) : Type
-| unknown {}           : PtrEqResult
+| unknown              : PtrEqResult
 | yesEqual (h : x = y) : PtrEqResult
 
 @[inline] unsafe def withPtrEqResultUnsafe {α : Type u} {β : Type v} [Subsingleton β] (a b : α) (k : PtrEqResult a b → β) : β :=
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 1d1e1200af..8f8006c796 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -160,8 +160,8 @@ variable  (rb  : β → β → Prop)
 
 -- Lexicographical order based on ra and rb
 inductive Lex : α × β → α × β → Prop
-| left  {a₁} (b₁) {a₂} (b₂) (h : ra a₁ a₂) : Lex (a₁, b₁) (a₂, b₂)
-| right (a) {b₁ b₂} (h : rb b₁ b₂)         : Lex (a, b₁)  (a, b₂)
+| left  {} {a₁} (b₁) {a₂} (b₂) (h : ra a₁ a₂) : Lex (a₁, b₁) (a₂, b₂)
+| right {} (a) {b₁ b₂} (h : rb b₁ b₂)         : Lex (a, b₁)  (a, b₂)
 
 -- relational product based on ra and rb
 inductive Rprod : α × β → α × β → Prop
@@ -262,8 +262,8 @@ variables {α : Sort u} {β : Sort v}
 
 -- Reverse lexicographical order based on r and s
 inductive RevLex (r  : α → α → Prop) (s  : β → β → Prop) : @PSigma α (fun a => β) → @PSigma α (fun a => β) → Prop
-| left  : ∀ {a₁ a₂ : α} (b : β), r a₁ a₂ → RevLex ⟨a₁, b⟩ ⟨a₂, b⟩
-| right : ∀ (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂ → RevLex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
+| left  {} : ∀ {a₁ a₂ : α} (b : β), r a₁ a₂ → RevLex ⟨a₁, b⟩ ⟨a₂, b⟩
+| right {} : ∀ (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂ → RevLex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
 end
 
 section