structure Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM.Context : Type

• semiringId : Nat

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM (α : Type) : Type

Equations

• Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM = ReaderT Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM.Context Lean.Meta.Grind.GoalM

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM.run {α : Type} (semiringId : Nat) (x : NonCommSemiringM α) : GoalM α

Equations

• Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM.run semiringId x = x { semiringId := semiringId }

instance Lean.Meta.Grind.Arith.CommRing.instMonadCanonNonCommSemiringM : MonadCanon NonCommSemiringM

Equations

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

def Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM.getSemiring : NonCommSemiringM Semiring

Equations

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

def Lean.Meta.Grind.Arith.CommRing.NonCommSemiringM.modifySemiring (f : Semiring → Semiring) : NonCommSemiringM Unit

Equations

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

instance Lean.Meta.Grind.Arith.CommRing.instMonadSemiringNonCommSemiringM : MonadSemiring NonCommSemiringM

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getTermNonCommSemiringId? (e : Expr) : GoalM (Option Nat)

Equations

• Lean.Meta.Grind.Arith.CommRing.getTermNonCommSemiringId? e = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.get' pure (Lean.PersistentHashMap.find? __do_lift.exprToNCSemiringId { expr := e })

def Lean.Meta.Grind.Arith.CommRing.setTermNonCommSemiringId (e : Expr) : NonCommSemiringM Unit

Equations

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

instance Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdNonCommSemiringM : MonadSetTermId NonCommSemiringM

Equations

• Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdNonCommSemiringM = { setTermId := fun (e : Lean.Expr) => Lean.Meta.Grind.Arith.CommRing.setTermNonCommSemiringId e }