Documentation

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

source
def Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.norm (c : DvdCnstr) :
DvdCnstr
Equations
    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
        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
            Instances For
              source
              def Lean.Meta.Grind.Arith.Cutsat.propagateNatDvd (e : Expr) :
              GoalM Unit
              Equations
                Instances For
                  source
                  def Lean.Meta.Grind.Arith.Cutsat.propagateDvd :
                  Propagator
                  Equations
                    Instances For