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

def Lean.Meta.Grind.Arith.CommRing.checkMaxDegree (p : Poly) : GoalM Bool

def Lean.Meta.Grind.Arith.CommRing.incSteps (n : Nat := 1) : 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.

  We also need it when destructively simplifying equations, i.e., when replacing an equation with its simplified form (EqCnstr.simplify and EqCnstr.simplifyBasis): the rewrite multiplies the equation by k₁ = k/gcd k k', and the result is weaker than the original equation when k₁ ≠ ±1. See Note at EqCnstr.simplify.

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

@[instance_reducible]

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

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

The Sym.Arith classification record of the current ring.

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

@[instance_reducible]

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

def Lean.Meta.Grind.Arith.CommRing.RingM.getCommRingState : RingM CommRingState

The per-goal solver state of the current ring.

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

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadCommRingStateRingM : MonadCommRingState RingM

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadGetVarRingM : Sym.Arith.MonadGetVar 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] [Sym.Arith.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] [Sym.Arith.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] [MonadRingState m] [MonadSetTermId m] (e : Expr) : m Var

@[instance_reducible]

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

@[instance_reducible]

instance Lean.Meta.Grind.Arith.CommRing.instMonadMkVarRingM : Sym.Arith.MonadMkVar RingM

Every term reified by the ring solver has been internalized, together with its subterms, before reification: the internalize hook runs after the core has created the ENodes of a term and its arguments, and solver-built terms are internalized where they are built.

def Lean.Meta.Grind.Arith.CommRing.getOne : RingM Expr

The numeral 1 of the current ring, internalized as a ring term of the current goal. The term is cached in the Sym.Arith record and thus shared by all goals, but internalization is per goal. The term may already be known to the core (e.g., as a subterm of a product) without having been registered by the ring solver, so the check is against the ring's own denote map.