chore: fix tests

tests/compiler/lazylist.lean

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 universes u v w
 
 inductive LazyList (α : Type u)
-| nil {}                        : LazyList
+| nil                           : LazyList
 | cons (hd : α) (tl : LazyList) : LazyList
 | delayed (t : Thunk LazyList)  : LazyList
 

tests/lean/run/125.lean

@@ -1,5 +1,5 @@
 class HasElems (α : Type) : Type := (elems : Array α)
-def elems (α : Type) [HasElems α] : Array α := HasElems.elems α
+def elems (α : Type) [HasElems α] : Array α := HasElems.elems
 
 inductive Foo : Type
 | mk1 : Bool → Foo

tests/lean/run/bigop.lean

@@ -18,7 +18,7 @@ def iota : Nat → Nat → List Nat
 def index_iota (m n : Nat) := iota m (n - m)
 
 class Enumerable (α : Type) :=
-(elems : List α)
+(elems {} : List α)
 
 instance : Enumerable Bool :=
 { elems := [false, true] }

tests/lean/run/coroutine.lean

@@ -1,8 +1,8 @@
 universes u v w r s
 
 inductive coroutineResultCore (coroutine : Type (max u v w)) (α : Type u) (δ : Type v) (β : Type w) : Type (max u v w)
-| done     {} : β → coroutineResultCore
-| yielded {}  : δ → coroutine → coroutineResultCore
+| done     : β → coroutineResultCore
+| yielded  : δ → coroutine → coroutineResultCore
 
 /--
    Asymmetric coroutines `coroutine α δ β` takes inputs of Type `α`, yields elements of Type `δ`,
@@ -15,7 +15,7 @@ inductive coroutineResultCore (coroutine : Type (max u v w)) (α : Type u) (δ :
    a calling routine.
  -/
 inductive coroutine (α : Type u) (δ : Type v) (β : Type w) : Type (max u v w)
-| mk    {} : (α → coroutineResultCore coroutine α δ β) → coroutine
+| mk    : (α → coroutineResultCore coroutine α δ β) → coroutine
 
 abbrev coroutineResult (α : Type u) (δ : Type v) (β : Type w) : Type (max u v w) :=
 coroutineResultCore (coroutine α δ β) α δ β
@@ -133,7 +133,7 @@ end coroutine
 
 /-- Auxiliary class for lifiting `yield` -/
 class monadCoroutine (α : outParam (Type u)) (δ : outParam (Type v)) (m : Type w → Type r) :=
-(yield {} : δ → m PUnit)
+(yield : δ → m PUnit)
 
 instance (α : Type u) (δ : Type v) : monadCoroutine α δ (coroutine α δ) :=
 { yield  := coroutine.yield }
@@ -149,8 +149,8 @@ open coroutine
 namespace ex1
 
 inductive tree (α : Type u)
-| leaf {} : tree
-| Node    : tree → α → tree → tree
+| leaf  : tree
+| Node  : tree → α → tree → tree
 
 /-- Coroutine as generators/iterators -/
 unsafe def visit {α : Type v} : tree α → coroutine Unit α Unit

tests/lean/run/frontend1.lean

@@ -101,8 +101,8 @@ def k : String := "hello"
 universes u
 
 class Monoid (α : Type u) :=
-(one {} : α)
-(mul    : α → α → α)
+(one : α)
+(mul : α → α → α)
 
 def m : Monoid Nat :=
 { one := 1, mul := Nat.mul }

tests/lean/run/new_compiler.lean

@@ -62,8 +62,8 @@ def bla' (i : Nat) (h : i > 0 ∧ i ≠ 10) : Nat :=
 @And.casesOn _ _ (fun _ => Nat) h (fun h₁ h₂ => aux i h₁ + aux i h₁)
 
 inductive vec (α : Type u) : Nat → Type u
-| nil {}  : vec 0
-| cons    : ∀ {n}, α → vec n → vec (Nat.succ n)
+| nil   : vec 0
+| cons  : ∀ {n}, α → vec n → vec (Nat.succ n)
 
 def vec.map {α β σ : Type u} (f : α → β → σ) : ∀ {n : Nat}, vec α n → vec β n → vec σ n
 | _, vec.nil, vec.nil                 => vec.nil

tests/lean/run/new_inductive.lean

@@ -42,7 +42,7 @@ with tst2 : Type
 namespace test
 
 inductive Rbnode (α : Type u)
-| leaf  {}                                                 : Rbnode
+| leaf                                                    : Rbnode
 | redNode   (lchild : Rbnode) (val : α) (rchild : Rbnode) : Rbnode
 | blackNode (lchild : Rbnode) (val : α) (rchild : Rbnode) : Rbnode
 

tests/lean/run/structInst2.lean

@@ -42,7 +42,7 @@ def optMonad2 {m} [Monad m] : Monad (OptionT m) :=
 def optAlt1 {m} [Monad m] : Alternative (OptionT m) :=
 { failure       := OptionT.fail,
   orelse        := OptionT.orelse,
-  toApplicative := Monad.toApplicative (OptionT m) } -- TODO: check toApplicative binder annotations
+  toApplicative := Monad.toApplicative }
 
 def optAlt2 {m} [Monad m] : Alternative (OptionT m) :=
 ⟨OptionT.fail, OptionT.orelse⟩ -- it works because it treats `toApplicative` as an instance implicit argument
@@ -50,4 +50,4 @@ def optAlt2 {m} [Monad m] : Alternative (OptionT m) :=
 def optAlt3 {m} [Monad m] : Alternative (OptionT2 m) :=
 { failure       := OptionT2.fail,
   orelse        := OptionT2.orelse,
-  toApplicative := Monad.toApplicative (OptionT2 m) }
+  toApplicative := Monad.toApplicative }

tests/lean/trust0/basic.lean

@@ -11,7 +11,7 @@ notation `ℕ` := Nat
 namespace Nat
 
 inductive lessThanOrEqual (a : ℕ) : ℕ → Prop
-| refl : lessThanOrEqual a
+| refl {} : lessThanOrEqual a
 | step : ∀ {b}, lessThanOrEqual b → lessThanOrEqual (succ b)
 
 @[elabAsEliminator]