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

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

Equations

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

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

The Sym.Arith classification record of the current non-commutative semiring.

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

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

The per-goal solver state of the current non-commutative semiring.

Equations

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

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

Equations

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

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadSemiringStateNonCommSemiringM : MonadSemiringState 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_reducible]

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 }

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadMkVarNonCommSemiringM : Sym.Arith.MonadMkVar NonCommSemiringM

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.