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

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

Instances

source
@[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.

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

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

Instances

source
@[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.

source
@[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.