Instances for grind.

@[implicit_reducible, instance 100]

instance Semiring.toGrindSemiring (α : Type u_1) [s : Semiring α] : Lean.Grind.Semiring α

@[implicit_reducible, instance 100]

instance CommSemiring.toGrindCommSemiring (α : Type u_1) [s : CommSemiring α] : Lean.Grind.CommSemiring α

@[implicit_reducible, instance 100]

instance Ring.toGrindRing (α : Type u_1) [s : Ring α] : Lean.Grind.Ring α

@[implicit_reducible, instance 100]

instance CommRing.toGrindCommRing (α : Type u_1) [s : CommRing α] : Lean.Grind.CommRing α

theorem Semiring.toGrindSemiring_ofNat (α : Type u_1) [Semiring α] (n : ℕ) : OfNat.ofNat n = ↑n