source
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)

Instances For

source
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 ()

Instances For

source
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 ()

Instances For

source
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.

Instances For

source
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.

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For