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

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.getCommSemiring : SemiringM CommSemiring

Equations

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

@[inline]

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

Equations

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

instance Lean.Meta.Grind.Arith.CommRing.instMonadCommSemiringSemiringM : MonadCommSemiring 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.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.getAddFn' {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] : m Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getMulFn' {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] : m Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getPowFn' {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadSemiring m] : m Expr

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getNatCastFn' {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadSemiring m] : m 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.

instance Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdSemiringM : MonadSetTermId SemiringM

Equations

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

def Lean.Meta.Grind.Arith.CommRing.mkSVarCore {m : Type → Type} [MonadLiftT GoalM m] [Monad m] [MonadSemiring m] [MonadSetTermId m] (e : Expr) : m Var

Similar to mkVarCore but for Semirings

Equations

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

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

Equations

• Lean.Meta.Grind.Arith.CommRing.mkSVar e = Lean.Meta.Grind.Arith.CommRing.mkSVarCore e

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

Equations

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