def Lean.Meta.Grind.Arith.CommRing.get' : GoalM State

Equations

• Lean.Meta.Grind.Arith.CommRing.get' = do let __do_lift ← get pure __do_lift.arith.ring

@[inline]

def Lean.Meta.Grind.Arith.CommRing.modify' (f : State → State) : GoalM Unit

Equations

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

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.incSteps : 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.

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

• getRing : m Ring

@[always_inline]

instance Lean.Meta.Grind.Arith.CommRing.instMonadGetRingOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadGetRing m] : MonadGetRing n

Equations

• Lean.Meta.Grind.Arith.CommRing.instMonadGetRingOfMonadLift m n = { getRing := liftM Lean.Meta.Grind.Arith.CommRing.getRing }

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

def Lean.Meta.Grind.Arith.CommRing.RingM.getRing : RingM Ring

Equations

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

instance Lean.Meta.Grind.Arith.CommRing.instMonadGetRingRingM : MonadGetRing RingM

Equations

• Lean.Meta.Grind.Arith.CommRing.instMonadGetRingRingM = { getRing := Lean.Meta.Grind.Arith.CommRing.RingM.getRing }

@[inline]

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

Equations

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

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

• semiringId : Nat

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.Arith.CommRing.SemiringM.run semiringId x = x { semiringId := semiringId }

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.CommRing.getSemiringId : SemiringM Nat

Equations

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

def Lean.Meta.Grind.Arith.CommRing.getSemiring : SemiringM Semiring

Equations

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

def Lean.Meta.Grind.Arith.CommRing.SemiringM.getRing : SemiringM Ring

Equations

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

instance Lean.Meta.Grind.Arith.CommRing.instMonadGetRingSemiringM : MonadGetRing SemiringM

Equations

• Lean.Meta.Grind.Arith.CommRing.instMonadGetRingSemiringM = { getRing := Lean.Meta.Grind.Arith.CommRing.SemiringM.getRing }

@[inline]

def Lean.Meta.Grind.Arith.CommRing.modifySemiring (f : Semiring → Semiring) : SemiringM Unit

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.setTermRingId (e : Expr) : RingM Unit

Equations

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

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

Equations

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

def Lean.Meta.Grind.Arith.CommRing.setTermSemiringId (e : Expr) : SemiringM Unit

Equations

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

def Lean.Meta.Grind.Arith.CommRing.nonzeroChar? {m : Type → Type} [Monad m] [MonadGetRing 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] [MonadGetRing 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.getRing 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.getRing 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.getRing 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.getRing pure (Lean.RBTree.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.