Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr

source
def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.norm (c : DvdCnstr) :
DvdCnstr
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
partial def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.applySubsts (c : DvdCnstr) :
GoalM DvdCnstr
source
partial def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.assert (c : DvdCnstr) :
GoalM Unit

Asserts divisibility constraint.

source
def Lean.Meta.Grind.Arith.Cutsat.propagateIntDvd (e : Expr) :
GoalM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Grind.Arith.Cutsat.propagateNatDvd (e : Expr) :
GoalM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Meta.Grind.Arith.Cutsat.propagateDvd :
Propagator
Equations
  • One or more equations did not get rendered due to their size.