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

- ringId : Nat

Instances For

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

Instances For

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

Instances For

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

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

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

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

Instances For

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

Instances For

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

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

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

Instances For

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

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

Instances For

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