diff --git a/tests/compiler/lazylist.lean b/tests/compiler/lazylist.lean index 8366517044..640c0570e2 100644 --- a/tests/compiler/lazylist.lean +++ b/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 diff --git a/tests/lean/run/125.lean b/tests/lean/run/125.lean index d9638ef7c8..9b53c99d91 100644 --- a/tests/lean/run/125.lean +++ b/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 diff --git a/tests/lean/run/bigop.lean b/tests/lean/run/bigop.lean index 49e1515dc8..c82622f44e 100644 --- a/tests/lean/run/bigop.lean +++ b/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] } diff --git a/tests/lean/run/coroutine.lean b/tests/lean/run/coroutine.lean index ad47b73df7..3516bb5787 100644 --- a/tests/lean/run/coroutine.lean +++ b/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 diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean index 3ab4afc61b..b6ae9f9811 100644 --- a/tests/lean/run/frontend1.lean +++ b/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 } diff --git a/tests/lean/run/new_compiler.lean b/tests/lean/run/new_compiler.lean index 92c532e7ad..951600cc37 100644 --- a/tests/lean/run/new_compiler.lean +++ b/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 diff --git a/tests/lean/run/new_inductive.lean b/tests/lean/run/new_inductive.lean index 11f6e58bb6..011d5666be 100644 --- a/tests/lean/run/new_inductive.lean +++ b/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 diff --git a/tests/lean/run/structInst2.lean b/tests/lean/run/structInst2.lean index f7a7af4d71..1b4113a19d 100644 --- a/tests/lean/run/structInst2.lean +++ b/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 } diff --git a/tests/lean/trust0/basic.lean b/tests/lean/trust0/basic.lean index ec1dba0fe2..bc20fec135 100644 --- a/tests/lean/trust0/basic.lean +++ b/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]