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.
Instances For
    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.
    Instances For
      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.
      Instances For
        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.
        Instances For
          source
          def Lean.Meta.Grind.Arith.Cutsat.propagateDvd :
          Propagator
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For