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

• semiringId : Nat

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.getSemiringId : SemiringM Nat

Equations

• Lean.Meta.Grind.Arith.CommRing.getSemiringId = do let __do_lift ← read pure __do_lift.semiringId

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

Equations

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

@[inline]

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

Equations

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

instance Lean.Meta.Grind.Arith.CommRing.instMonadCanonSemiringM : MonadCanon SemiringM

Equations

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

def Lean.Meta.Grind.Arith.CommRing.SemiringM.getCommRing : SemiringM CommRing

Equations

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

def Lean.Meta.Grind.Arith.CommRing.SemiringM.modifyCommRing (f : CommRing → CommRing) : SemiringM Unit

Equations

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

instance Lean.Meta.Grind.Arith.CommRing.instMonadCommRingSemiringM : MonadCommRing SemiringM

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getAddFn' : SemiringM Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getMulFn' : SemiringM Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getPowFn' : SemiringM Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getNatCastFn' : SemiringM Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getToQFn : SemiringM Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getAddRightCancelInst? : SemiringM (Option Expr)

Equations

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

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

Equations

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

def Lean.Meta.Grind.Arith.CommRing.setTermSemiringId (e : Expr) : SemiringM Unit

Equations

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

def Lean.Meta.Grind.Arith.CommRing.mkSVar (e : Expr) : SemiringM Var

Similar to mkVar but for Semirings

Equations

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

def Lean.Grind.Ring.OfSemiring.Expr.denoteAsRingExpr (e : Meta.Grind.Arith.CommRing.SemiringExpr) : Meta.Grind.Arith.CommRing.SemiringM Lean.Expr

Equations

• Lean.Grind.Ring.OfSemiring.Expr.denoteAsRingExpr e = do let __do_lift ← Lean.Grind.Ring.OfSemiring.Expr.denoteAsRingExpr.go✝ e liftM (Lean.Meta.Grind.shareCommon __do_lift)