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

- semiringId : Nat

Instances For

source
@[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

Instances For

source
@[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 }

Instances For

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

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

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

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

Instances For

source
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.

Instances For

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

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

source
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 })

Instances For

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

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

Instances For

source
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 }