CommRing interface for cutsat. We use it to normalize nonlinear polynomials.

def Int.Linear.Poly.isNonlinear (p : Poly) : Lean.Meta.Grind.GoalM Bool

Returns true if p contains a nonlinear monomial.

Equations

• One or more equations did not get rendered due to their size.
• p.isNonlinear = pure false

def Int.Linear.Poly.getGeneration (p : Poly) : Lean.Meta.Grind.GoalM Nat

Equations

• p.getGeneration = Int.Linear.Poly.getGeneration.go p 0

def Int.Linear.Poly.getGeneration.go : Poly → Nat → Lean.Meta.Grind.GoalM Nat

Equations

• One or more equations did not get rendered due to their size.
• Int.Linear.Poly.getGeneration.go (Int.Linear.Poly.num k) x✝ = pure x✝

def Lean.Meta.Grind.Arith.Cutsat.getIntRingId? : GoalM (Option Nat)

Equations

• Lean.Meta.Grind.Arith.Cutsat.getIntRingId? = do let __do_lift ← liftM Lean.Meta.Grind.getIntExpr Lean.Meta.Grind.Arith.CommRing.getRingId? __do_lift

def Int.Linear.Poly.normCommRing? (p : Poly) : Lean.Meta.Grind.GoalM (Option (Lean.Meta.Grind.Arith.CommRing.RingExpr × Lean.Grind.CommRing.Poly × Poly))

Normalize the polynomial using CommRing

Equations

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