def Lean.Meta.Grind.Arith.CommRing.checkMaxSteps : GoalM Bool

def Lean.Meta.Grind.Arith.CommRing.incSteps : GoalM Unit

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

• ringId : Nat
• checkCoeffDvd : Bool

  If checkCoeffDvd is true, then when using a polynomial k*m - p to simplify .. + k'*m*m_2 + ..., the substitution is performed IF

  • k divides k', OR
  • Ring implements NoNatZeroDivisors.

  We need this check when simplifying disequalities. In this case, if we perform the simplification anyway, we may end up with a proof that k * q = 0, but we cannot deduce q = 0 since the ring does not implement NoNatZeroDivisors See comment at PolyDerivation.

@[reducible, inline]

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

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

@[reducible, inline]

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

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.getRingId : RingM Nat

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadCanonRingM : MonadCanon RingM

def Lean.Meta.Grind.Arith.CommRing.RingM.getCommRing : RingM CommRing

def Lean.Meta.Grind.Arith.CommRing.RingM.modifyCommRing (f : CommRing → CommRing) : RingM Unit

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadCommRingRingM : MonadCommRing RingM

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.withCheckCoeffDvd {α : Type} (x : RingM α) : RingM α

def Lean.Meta.Grind.Arith.CommRing.checkCoeffDvd : RingM Bool

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

def Lean.Meta.Grind.Arith.CommRing.nonzeroChar? {m : Type → Type} [Monad m] [MonadRing m] : m (Option Nat)

Returns some c if the current ring has a nonzero characteristic c.

def Lean.Meta.Grind.Arith.CommRing.nonzeroCharInst? {m : Type → Type} [Monad m] [MonadRing m] : m (Option (Expr × Nat))

Returns some (charInst, c) if the current ring has a nonzero characteristic c.

def Lean.Meta.Grind.Arith.CommRing.noZeroDivisorsInst? : RingM (Option Expr)

def Lean.Meta.Grind.Arith.CommRing.noZeroDivisors : RingM Bool

Returns true if the current ring satisfies the property

∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0

def Lean.Meta.Grind.Arith.CommRing.hasChar : RingM Bool

Returns true if the current ring has a IsCharP instance.

def Lean.Meta.Grind.Arith.CommRing.getCharInst : RingM (Expr × Nat)

Returns the pair (charInst, c). If the ring does not have a IsCharP instance, then throws internal error.

def Lean.Meta.Grind.Arith.CommRing.isField : RingM Bool

def Lean.Meta.Grind.Arith.CommRing.isQueueEmpty : RingM Bool

def Lean.Meta.Grind.Arith.CommRing.getNext? : RingM (Option EqCnstr)

class Lean.Meta.Grind.Arith.CommRing.MonadSetTermId (m : Type → Type) : Type

• setTermId : Expr → m Unit

def Lean.Meta.Grind.Arith.CommRing.setTermRingId (e : Expr) : RingM Unit

def Lean.Meta.Grind.Arith.CommRing.mkVarCore {m : Type → Type} [MonadLiftT GoalM m] [Monad m] [MonadRing m] [MonadSetTermId m] (e : Expr) : m Var

@[implicit_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadSetTermIdRingM : MonadSetTermId RingM

def Lean.Meta.Grind.Arith.CommRing.mkVar (e : Expr) : RingM Var