class Lean.Meta.Grind.Arith.CommRing.MonadRing (m : Type → Type) : Type

• getRing : m Ring
• modifyRing : (Ring → Ring) → m Unit

@[implicit_reducible, always_inline]

instance Lean.Meta.Grind.Arith.CommRing.instMonadRingOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadRing m] : MonadRing n

class Lean.Meta.Grind.Arith.CommRing.MonadCommRing (m : Type → Type) : Type

• getCommRing : m CommRing
• modifyCommRing : (CommRing → CommRing) → m Unit

@[implicit_reducible, always_inline]

instance Lean.Meta.Grind.Arith.CommRing.instMonadCommRingOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadCommRing m] : MonadCommRing n

@[implicit_reducible, always_inline]

instance Lean.Meta.Grind.Arith.CommRing.instMonadRingOfMonadOfMonadCommRing (m : Type → Type) [Monad m] [MonadCommRing m] : MonadRing m