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

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

@[instance_reducible, always_inline]

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

Equations

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

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

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

@[instance_reducible, always_inline]

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

Equations

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

@[instance_reducible, always_inline]

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

Equations

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