Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.MonadSemiring

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

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

Instances

@[always_inline]

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

MonadSemiring n

Equations

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

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

Instances

@[always_inline]

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

MonadCommSemiring n

Equations

@[always_inline]

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

MonadSemiring m

Equations