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

• ringId : Nat

@[reducible, inline]

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

We don't want to keep carrying the RingId around.

Equations

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

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.Arith.CommRing.NonCommRingM.run ringId x = x { ringId := ringId }

instance Lean.Meta.Grind.Arith.CommRing.instMonadCanonNonCommRingM : MonadCanon NonCommRingM

Equations

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

def Lean.Meta.Grind.Arith.CommRing.NonCommRingM.getRing : NonCommRingM Ring

Equations

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

def Lean.Meta.Grind.Arith.CommRing.NonCommRingM.modifyRing (f : Ring → Ring) : NonCommRingM Unit

Equations

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

instance Lean.Meta.Grind.Arith.CommRing.instMonadRingNonCommRingM : MonadRing NonCommRingM

Equations

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

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

Equations

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

def Lean.Meta.Grind.Arith.CommRing.setTermNonCommRingId (e : Expr) : NonCommRingM Unit

Equations

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

instance Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdNonCommRingM : MonadSetTermId NonCommRingM

Equations

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