class Lean.Meta.Sym.Arith.MonadSemiring (m : Type → Type) : Type

• getSemiring : m Semiring
• modifySemiring : (Semiring → Semiring) → m Unit

@[implicit_reducible, always_inline]

instance Lean.Meta.Sym.Arith.instMonadSemiringOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadSemiring m] : MonadSemiring n

class Lean.Meta.Sym.Arith.MonadCommSemiring (m : Type → Type) : Type

• getCommSemiring : m CommSemiring
• modifyCommSemiring : (CommSemiring → CommSemiring) → m Unit

@[implicit_reducible, always_inline]

instance Lean.Meta.Sym.Arith.instMonadCommSemiringOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadCommSemiring m] : MonadCommSemiring n

@[implicit_reducible, always_inline]

instance Lean.Meta.Sym.Arith.instMonadSemiringOfMonadOfMonadCommSemiring (m : Type → Type) [Monad m] [MonadCommSemiring m] : MonadSemiring m