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

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

Equations

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

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

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

def Lean.Meta.Grind.Arith.CommRing.NonCommRingM.getRingState : NonCommRingM RingState

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

Equations

• Lean.Meta.Grind.Arith.CommRing.NonCommRingM.getRingState = do let __do_lift ← liftM Lean.Meta.Grind.Arith.CommRing.get' let __do_lift_1 ← read pure (__do_lift.getNCRing __do_lift_1.ringId)

def Lean.Meta.Grind.Arith.CommRing.NonCommRingM.modifyRingState (f : RingState → RingState) : NonCommRingM Unit

Equations

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

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadRingStateNonCommRingM : MonadRingState NonCommRingM

Equations

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

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadGetVarNonCommRingM : Sym.Arith.MonadGetVar 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_reducible]

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 }

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadMkVarNonCommRingM : Sym.Arith.MonadMkVar NonCommRingM

Equations

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