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.isSorted.go : Option Var → Poly → Bool

Equations

• Lean.Grind.Linarith.Poly.isSorted.go x✝ Lean.Grind.Linarith.Poly.nil = true
• Lean.Grind.Linarith.Poly.isSorted.go none (Lean.Grind.Linarith.Poly.add k y p) = Lean.Grind.Linarith.Poly.isSorted.go (some y) p
• Lean.Grind.Linarith.Poly.isSorted.go (some x_2) (Lean.Grind.Linarith.Poly.add k y p) = (decide (x_2 > y) && Lean.Grind.Linarith.Poly.isSorted.go (some y) 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.checkOccs.go (y : Var) (p : Poly) : Meta.Grind.Arith.Linear.LinearM Unit

Equations

• One or more equations did not get rendered due to their size.
• Lean.Grind.Linarith.Poly.checkOccs.go y p = 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.