From 7ae5a5ea0c1a91f84b729a20e440502f09fbbce3 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 3 Sep 2024 14:54:09 +1000
Subject: [PATCH] fix tests

---
 tests/lean/1870.lean                          | 9 ---------
 tests/lean/1870.lean.expected.out             | 6 +++---
 tests/lean/isDefEqOffsetBug.lean.expected.out | 2 +-
 tests/lean/run/KyleAlgAbbrev.lean             | 2 --
 4 files changed, 4 insertions(+), 15 deletions(-)

diff --git a/tests/lean/1870.lean b/tests/lean/1870.lean
index fdd27cdda8d4..734365b486d7 100644
--- a/tests/lean/1870.lean
+++ b/tests/lean/1870.lean
@@ -1,12 +1,3 @@
-class Zero.{u} (α : Type u) where
-  zero : α
-
-instance Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
-  ofNat := ‹Zero α›.1
-
-instance Zero.ofOfNat0 {α} [OfNat α (nat_lit 0)] : Zero α where
-  zero := 0
-
 class One (α : Type u) where
   one : α
 
diff --git a/tests/lean/1870.lean.expected.out b/tests/lean/1870.lean.expected.out
index 133830702147..a6f2f8e7561c 100644
--- a/tests/lean/1870.lean.expected.out
+++ b/tests/lean/1870.lean.expected.out
@@ -1,15 +1,15 @@
-1870.lean:21:2-21:35: error: type mismatch
+1870.lean:12:2-12:35: error: type mismatch
   congrArg (@OfNat.ofNat Nat 0) (congrArg (@Zero.toOfNat0 Nat) ?_)
 has type
   OfNat.ofNat 0 = OfNat.ofNat 0 : Prop
 but is expected to have type
   OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
-1870.lean:25:2-25:16: error: tactic 'apply' failed, failed to unify
+1870.lean:16:2-16:16: error: tactic 'apply' failed, failed to unify
   ?f ?a₁ = ?f ?a₂
 with
   OfNat.ofNat 0 = OfNat.ofNat 1
 ⊢ OfNat.ofNat 0 = OfNat.ofNat 1
-1870.lean:30:2-30:16: error: tactic 'apply' failed, failed to unify
+1870.lean:21:2-21:16: error: tactic 'apply' failed, failed to unify
   ?f ?a₁ = ?f ?a₂
 with
   OfNat.ofNat 0 = OfNat.ofNat 1
diff --git a/tests/lean/isDefEqOffsetBug.lean.expected.out b/tests/lean/isDefEqOffsetBug.lean.expected.out
index 1f3153cf0743..14aea3e05373 100644
--- a/tests/lean/isDefEqOffsetBug.lean.expected.out
+++ b/tests/lean/isDefEqOffsetBug.lean.expected.out
@@ -1,4 +1,4 @@
-isDefEqOffsetBug.lean:27:2-27:5: error: type mismatch
+isDefEqOffsetBug.lean:19:2-19:5: error: type mismatch
   rfl
 has type
   0 + 0 = 0 + 0 : Prop
diff --git a/tests/lean/run/KyleAlgAbbrev.lean b/tests/lean/run/KyleAlgAbbrev.lean
index a8cb2a7a2f2e..0add04690f59 100644
--- a/tests/lean/run/KyleAlgAbbrev.lean
+++ b/tests/lean/run/KyleAlgAbbrev.lean
@@ -21,8 +21,6 @@ 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