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_reducible]

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

Equations

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

def Lean.Meta.Grind.Arith.CommRing.SemiringM.getCommSemiring : SemiringM Sym.Arith.CommSemiring

The Sym.Arith classification record of the current semiring.

Equations

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

@[inline]

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

Equations

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

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadCommSemiringSemiringM : Sym.Arith.MonadCommSemiring SemiringM

Equations

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

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

The Sym.Arith record of the envelope ring OfSemiring.Q of the current semiring.

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

def Lean.Meta.Grind.Arith.CommRing.SemiringM.getSemiringState : SemiringM SemiringState

The per-goal solver state of the current semiring.

Equations

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

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

Equations

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

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadSemiringStateSemiringM : MonadSemiringState SemiringM

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_reducible]

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] [MonadSemiringState 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.

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadMkVarSemiringM : Sym.Arith.MonadMkVar SemiringM

Semiring terms are reified only by the internalize hook, after the core has created the ENodes of the term and of all its subterms. So every variable created here is already internalized, and there is no generation to assign.

Equations

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

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

Denotes e in the envelope ring OfSemiring.Q. The atoms toQ x are new terms, so they are internalized here with generation gen.

Equations

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