Skip to content

Commit 106179f

Browse files
committed
fix test
1 parent 7530423 commit 106179f

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

BatteriesTest/instances.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ error: type class instance expected
1313
info: 2 instances:
1414
1515
instAddNat : Add Nat
16-
Lean.Grind.CommRing.toAdd.{u} {α : Type u} [self : Lean.Grind.CommRing α] : Add α
16+
(prio 100) Lean.Grind.CommRing.toAdd.{u} {α : Type u} [self : Lean.Grind.CommRing α] : Add α
1717
-/
1818
#guard_msgs in
1919
#instances Add Nat

0 commit comments

Comments
 (0)