cleanup tests

Author: kim-em

tests/lean/2178.lean

@@ -1,5 +1,3 @@
-class Zero (α : Type u) where
-  zero : α
 class AddZeroClass (M : Type u) extends Zero M, Add M
 class AddMonoid (M : Type u) extends AddZeroClass M where
   nsmul : Nat → M → M := fun _ _ => Zero.zero

tests/lean/diamond10.lean

@@ -1,6 +1,3 @@
-class Zero (A : Type u) where zero : A
-instance {A} [Zero A] : OfNat A (nat_lit 0) := ⟨Zero.zero⟩
-
 class AddMonoid (A : Type u) extends Add A, Zero A
 class Semiring (R : Type u) extends AddMonoid R
 class SubNegMonoid (A : Type u) extends AddMonoid A, Neg A

tests/lean/diamond7.lean

@@ -39,12 +39,6 @@ class AddSemigroup (α : Type u) extends Add α where
 class AddCommSemigroup (α : Type u) extends AddSemigroup α where
   add_comm (a b : α) : a + b = b + a
 
-class Zero (α : Type u) where
-  zero : α
-
-instance [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := Zero.zero
-
 class AddMonoid (α : Type u) extends AddSemigroup α, Zero α where
   zero_add (a : α) : 0 + a = a
   add_zero (a : α) : a + 0 = a

tests/lean/diamond8.lean

@@ -1,9 +1,6 @@
 class One (M : Type u) where one : M
 instance {M} [One M] : OfNat M (nat_lit 1) := ⟨One.one⟩
 
-class Zero (A : Type u) where zero : A
-instance {A} [Zero A] : OfNat A (nat_lit 0) := ⟨Zero.zero⟩
-
 class Monoid (M : Type u) extends Mul M, One M where
   mul_one (m : M) : m * 1 = m
 

tests/lean/diamond9.lean

@@ -1,6 +1,3 @@
-class Zero (A : Type u) where zero : A
-instance {A} [Zero A] : OfNat A (nat_lit 0) := ⟨Zero.zero⟩
-
 class AddGroup (A : Type u) extends Zero A where
   gsmul : Int → A → A
   gsmul_zero' : ∀ a, gsmul 0 a = 0

tests/lean/isDefEqOffsetBug.lean

@@ -1,11 +1,3 @@
-class Zero (α : Type u) where
-  zero : α
-
-export Zero (zero)
-
-instance [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := zero
-
 class AddGroup (α : Type u) extends Add α, Zero α, Neg α where
   addAssoc : {a b c : α} → a + b + c = a + (b + c)
   zeroAdd  : {a : α} → 0 + a = a

tests/lean/run/2265.lean

@@ -1,3 +1,3 @@
-class NeZero (n : Nat) : Prop
-theorem mul_div (m n : Nat) [NeZero n] : (m * n) / n = m := sorry
-example [NeZero n] : (m * n) / n = m := by simp [mul_div m _]
+class NeZero' (n : Nat) : Prop
+theorem mul_div (m n : Nat) [NeZero' n] : (m * n) / n = m := sorry
+example [NeZero' n] : (m * n) / n = m := by simp [mul_div m _]

tests/lean/run/2461.lean

@@ -1,8 +1,5 @@
 section algebra_hierarchy_classes_to_comm_ring
 
-class Zero (α : Type) where
-  zero : α
-
 class One (α : Type) where
   one : α
 

tests/lean/run/326.lean

@@ -1,5 +1,3 @@
-abbrev Zero α := OfNat α (nat_lit 0)
-
 class Monoid (α : Type u) [Zero α] extends Add α where
   zero_add (a : α) : 0 + a = a
   add_zero (a : α) : a + 0 = a

tests/lean/run/3313.lean

@@ -1,6 +1,3 @@
-class Zero (α : Type) where
-  zero : α
-
 class AddCommGroup (α : Type) extends Zero α where
 
 class Ring (α : Type) extends Zero α, AddCommGroup α

tests/lean/run/3807.lean

@@ -93,12 +93,6 @@ section Mathlib.Init.ZeroOne
 
 set_option autoImplicit true
 
-class Zero.{u} (α : Type u) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 class One (α : Type u) where
   one : α
 

tests/lean/run/788.lean

@@ -3,3 +3,4 @@ example : (0 : Nat) = Nat.zero := by
 
 example : (0 : Fin 9) = (Fin.ofNat 0) := by
   simp only [OfNat.ofNat]
+  rfl

tests/lean/run/KyleAlg.lean

@@ -21,13 +21,8 @@ export One (one)
 instance [One α] : OfNat α (nat_lit 1) where
     ofNat := one
 
-class Zero (α : Type u) where
-    zero : α
 export Zero (zero)
 
-instance [Zero α] : OfNat α (nat_lit 0) where
-    ofNat := zero
-
 class MulComm (α : Type u) [Mul α] : Prop where
     mulComm : {a b : α} → a * b = b * a
 export MulComm (mulComm)

tests/lean/run/binop_binrel_perf_issue.lean

@@ -26,12 +26,6 @@ section Mathlib.Init.ZeroOne
 
 set_option autoImplicit true
 
-class Zero.{u} (α : Type u) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 class One (α : Type u) where
   one : α
 

tests/lean/run/dsimpNatLitIssue.lean

@@ -1,11 +1,5 @@
 variable {R M : Type}
 
-class Zero (α : Type) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 /-- Typeclass for the `⊥` (`\bot`) notation -/
 class Bot (α : Type) where
   /-- The bot (`⊥`, `\bot`) element -/

tests/lean/run/mathlibetaissue.lean

@@ -44,10 +44,6 @@ end Std.Classes.RatCast
 
 section Mathlib.Init.ZeroOne
 
-class Zero.{u} (α : Type u) where
-  zero : α
-instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
 class One (α : Type u) where
   one : α
 instance One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1) where

tests/lean/run/matrix.lean

@@ -10,15 +10,6 @@ instance [OfNat α (nat_lit 1)] : One α where
 instance [One α] : OfNat α (nat_lit 1) where
   ofNat := One.one
 
-class Zero (α : Type u) where
-  zero : α
-
-instance [OfNat α (nat_lit 0)] : Zero α where
-  zero := 0
-
-instance [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := Zero.zero
-
 /- Simple Matrix -/
 
 def Matrix (m n : Nat) (α : Type u) : Type u :=

tests/lean/run/ofNatNormNum.lean

@@ -6,15 +6,9 @@ export OfNatSound (ofNat_add)
 theorem ex1 {α : Type u} [Add α] [(n : Nat) → OfNat α n] [OfNatSound α] : (10000000 : α) + 10000000 = 20000000 :=
   ofNat_add ..
 
-class Zero (α : Type u) where
-  zero : α
-
 class One (α : Type u) where
   one : α
 
-instance [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := Zero.zero
-
 instance [One α] : OfNat α (nat_lit 1) where
   ofNat := One.one
 

tests/lean/run/ofNat_class.lean

@@ -12,4 +12,4 @@ local macro "ofNat_class" Class:ident n:num : command =>
   instance {α} [OfNat α (nat_lit $n)] : $Class α where
     $field:ident := $n)
 
-ofNat_class Zero 0
+ofNat_class Zero' 0

tests/lean/run/scopedunifhint.lean

@@ -23,30 +23,32 @@ scoped unif_hint (s : Magma) where
 
 end Algebra
 
+set_option pp.mvars false
+
 def x : Nat := 10
 
 /--
 error: application type mismatch
-  mul ?m.742 x
+  mul ?_ x
 argument
   x
 has type
   Nat : Type
 but is expected to have type
-  ?m.730.α : Type ?u.729
+  ?_.α : Type _
 -/
 #guard_msgs in
 #check mul x x           -- Error: unification hint is not active
 
 /--
 error: application type mismatch
-  mul ?m.833 (x, x)
+  mul ?_ (x, x)
 argument
   (x, x)
 has type
   Nat × Nat : Type
 but is expected to have type
-  ?m.817.α : Type ?u.816
+  ?_.α : Type _
 -/
 #guard_msgs in
 #check mul (x, x) (x, x) -- Error: no unification hint
@@ -55,13 +57,13 @@ local infix:65 (priority := high) "*" => mul
 
 /--
 error: application type mismatch
-  ?m.2484*x
+  ?_*x
 argument
   x
 has type
   Nat : Type
 but is expected to have type
-  ?m.2472.α : Type ?u.2471
+  ?_.α : Type _
 -/
 #guard_msgs in
 #check x*x -- Error: unification hint is not active
@@ -73,13 +75,13 @@ open Algebra -- activate unification hints
 
 /--
 error: application type mismatch
-  ?m.2585*(x, x)
+  ?_*(x, x)
 argument
   (x, x)
 has type
   Nat × Nat : Type
 but is expected to have type
-  ?m.2565.α : Type ?u.2564
+  ?_.α : Type _
 -/
 #guard_msgs in
 #check mul (x, x) (x, x) -- still error
@@ -101,13 +103,13 @@ end Sec1
 
 /--
 error: application type mismatch
-  ?m.2832*(x, x)
+  ?_*(x, x)
 argument
   (x, x)
 has type
   Nat × Nat : Type
 but is expected to have type
-  ?m.2812.α : Type ?u.2811
+  ?_.α : Type _
 -/
 #guard_msgs in
 #check (x, x) * (x, x) -- error, local hint is not active after end of section anymore

tests/lean/run/unfoldPartialRegression.lean

@@ -1,11 +1,5 @@
 universe u
 
-class Zero (α : Type u) where
-  zero : α
-
-instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
 class One (α : Type u) where
   one : α