Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr

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

    Given an equation c₁ containing the monomial a*x, and an inequality 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
      def Int.Linear.Poly.isNegEq (p₁ p₂ : Poly) :
      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Given an expression e that is in True (or False equivalence class), if e is an integer inequality, asserts it to the cutsat state.

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