fix tests

leanprover · Sep 10, 2024 · ccee4a6 · ccee4a6
1 parent 994a5b5
commit ccee4a6
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 15 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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