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

Equations

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

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

Equations

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

def Lean.Meta.Grind.Arith.CommRing.incSteps (n : Nat := 1) : GoalM Unit

Equations

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

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.

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.Arith.CommRing.getRingId = do let __do_lift ← read pure __do_lift.ringId

@[instance_reducible]

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

Equations

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

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.Arith.CommRing.withCheckCoeffDvd x = withReader (fun (ctx : Lean.Meta.Grind.Arith.CommRing.RingM.Context) => { ringId := ctx.ringId, checkCoeffDvd := true }) x

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

Equations

• Lean.Meta.Grind.Arith.CommRing.checkCoeffDvd = do let __do_lift ← read pure __do_lift.checkCoeffDvd

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

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

• Lean.Meta.Grind.Arith.CommRing.noZeroDivisorsInst? = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getCommRing pure __do_lift.noZeroDivInst?

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

Equations

• Lean.Meta.Grind.Arith.CommRing.noZeroDivisors = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getCommRing pure __do_lift.noZeroDivInst?.isSome

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

Returns true if the current ring has a IsCharP instance.

Equations

• Lean.Meta.Grind.Arith.CommRing.hasChar = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getRing pure __do_lift.charInst?.isSome

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.

Equations

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

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

Equations

• Lean.Meta.Grind.Arith.CommRing.isField = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getCommRing pure __do_lift.fieldInst?.isSome

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

Equations

• Lean.Meta.Grind.Arith.CommRing.isQueueEmpty = do let __do_lift ← Lean.Meta.Grind.Arith.CommRing.getCommRing pure (Std.TreeSet.isEmpty __do_lift.queue)

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

Equations

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

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

Equations

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

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

Equations

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

@[instance_reducible]

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

Equations

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

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

Equations

• Lean.Meta.Grind.Arith.CommRing.mkVar e = Lean.Meta.Grind.Arith.CommRing.mkVarCore e