def Lean.Grind.Linarith.Poly.isSorted (p : Poly) : Bool

Returns true if the variables in the given polynomial are sorted in decreasing order.

Equations

• p.isSorted = Lean.Grind.Linarith.Poly.isSorted.go✝ none p

def Lean.Grind.Linarith.Poly.checkCoeffs : Poly → Bool

Returns true if all coefficients are not 0.

Equations

• Lean.Grind.Linarith.Poly.nil.checkCoeffs = true
• (Lean.Grind.Linarith.Poly.add k v p).checkCoeffs = (k != 0 && p.checkCoeffs)

def Lean.Grind.Linarith.Poly.checkOccs (p : Poly) : Meta.Grind.Arith.Linear.LinearM Unit

Equations

• (Lean.Grind.Linarith.Poly.add k x p_2).checkOccs = Lean.Grind.Linarith.Poly.checkOccs.go✝ x p_2
• p.checkOccs = pure ()

def Lean.Grind.Linarith.Poly.checkNoElimVars (p : Poly) : Meta.Grind.Arith.Linear.LinearM Unit

Equations

• One or more equations did not get rendered due to their size.
• p.checkNoElimVars = pure ()

def Lean.Grind.Linarith.Poly.checkCnstrOf (p : Poly) (x : Var) : Meta.Grind.Arith.Linear.LinearM Unit

Equations

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

def Lean.Meta.Grind.Arith.Linear.checkLeCnstrs (css : PArray (PArray IneqCnstr)) (isLower : Bool) : LinearM Unit

Equations

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

def Lean.Meta.Grind.Arith.Linear.checkLowers : LinearM Unit

Equations

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

def Lean.Meta.Grind.Arith.Linear.checkUppers : LinearM Unit

Equations

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

def Lean.Meta.Grind.Arith.Linear.checkDiseqCnstrs : LinearM Unit

Equations

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

def Lean.Meta.Grind.Arith.Linear.checkVars : LinearM Unit

Equations

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

def Lean.Meta.Grind.Arith.Linear.checkStructInvs : LinearM Unit

Equations

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

def Lean.Meta.Grind.Arith.Linear.checkInvariants : GoalM Unit

Equations

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