Skip to content

Commit 39c616f

Browse files
committed
fix test
1 parent 2ebecea commit 39c616f

File tree

1 file changed

+0
-2
lines changed

1 file changed

+0
-2
lines changed

BatteriesTest/instances.lean

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,6 @@ error: type class instance expected
1313
info: 4 instances:
1414
1515
instAddNat : Add Nat
16-
(prio 100) Lean.Grind.IntModule.toAdd.{u} {M : Type u} [self : Lean.Grind.IntModule M] : Add M
17-
(prio 100) Lean.Grind.NatModule.toAdd.{u} {M : Type u} [self : Lean.Grind.NatModule M] : Add M
1816
(prio 100) Lean.Grind.Semiring.toAdd.{u} {α : Type u} [self : Lean.Grind.Semiring α] : Add α
1917
(prio 100) Lean.Grind.IntModule.toAdd.{u} {M : Type u} [self : Lean.Grind.IntModule M] : Add M
2018
(prio 100) Lean.Grind.NatModule.toAdd.{u} {M : Type u} [self : Lean.Grind.NatModule M] : Add M

0 commit comments

Comments
 (0)