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

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

@[implicit_reducible, always_inline]

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

Equations

• One or more equations did not get rendered due to their size.

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

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

@[implicit_reducible, always_inline]

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

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible, always_inline]

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

Equations

• One or more equations did not get rendered due to their size.