def Int.Linear.Poly.checkCoeffs : Poly → Bool

Returns true if all coefficients are not 0.

Equations

• (Int.Linear.Poly.num k).checkCoeffs = true
• (Int.Linear.Poly.add k v p).checkCoeffs = (k != 0 && p.checkCoeffs)

def Int.Linear.Poly.checkNoElimVars (p : Poly) : Lean.Meta.Grind.GoalM Unit

Equations

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

def Int.Linear.Poly.checkOccs (p : Poly) : Lean.Meta.Grind.GoalM Unit

Equations

• (Int.Linear.Poly.add k x p_2).checkOccs = Int.Linear.Poly.checkOccs.go✝ x p_2
• p.checkOccs = pure ()

def Int.Linear.Poly.checkCnstrOf (p : Poly) (x : Var) : Lean.Meta.Grind.GoalM Unit

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.checkLeCnstrs (css : PArray (PArray LeCnstr)) (isLower : Bool) : GoalM Unit

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.checkLowers : GoalM Unit

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.checkUppers : GoalM Unit

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.checkDvds : GoalM Unit

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.checkVars : GoalM Unit

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.checkElimEqs : GoalM Unit

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.checkElimStack : GoalM Unit

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.checkDiseqCnstrs : GoalM Unit

Equations

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

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

Equations

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