def Lean.Meta.Grind.Arith.Cutsat.mkDvdCnstr (d : Int) (p : Poly) (h : DvdCnstrProof) : GoalM DvdCnstr

Equations

• Lean.Meta.Grind.Arith.Cutsat.mkDvdCnstr d p h = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.mkCnstrId pure { d := d, p := p, h := h, id := __do_lift }

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.norm (c : DvdCnstr) : GoalM DvdCnstr

Equations

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

def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : DvdCnstr) : GoalM DvdCnstr

Given an equation c₁ containing the monomial a*x, and a divisibility constraint c₂ containing the monomial b*x, eliminate x by applying substitution.

Equations

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

partial def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.applySubsts (c : DvdCnstr) : GoalM DvdCnstr

partial def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.assert (c : DvdCnstr) : GoalM Unit

Asserts divisibility constraint.

def Lean.Meta.Grind.Arith.Cutsat.propagateDvd : Propagator

Equations

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