Documentation

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

source
def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.norm (c : LeCnstr) :
LeCnstr
Instances For
    source
    def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : LeCnstr) :
    GoalM LeCnstr

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

    Instances For
      source
      partial def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.applySubsts (c : LeCnstr) :
      GoalM LeCnstr
      source
      def Int.Linear.Poly.isNegEq (p₁ p₂ : Poly) :
      Bool
      Instances For
        source
        def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.erase (c : LeCnstr) :
        GoalM Unit
        Instances For
          source
          @[export lean_grind_cutsat_assert_le]
          def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.assertImpl (c : LeCnstr) :
          GoalM Unit
          Instances For
            source
            def Lean.Meta.Grind.Arith.Cutsat.propagateIntLe (e : Expr) (eqTrue : Bool) :
            GoalM Unit

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

            Instances For
              source
              def Lean.Meta.Grind.Arith.Cutsat.propagateNatLe (e : Expr) (eqTrue : Bool) :
              GoalM Unit
              Instances For
                source
                def Lean.Meta.Grind.Arith.Cutsat.propagateToIntLe (e : Expr) (eqTrue : Bool) :
                ToIntM Unit
                Instances For
                  source
                  def Lean.Meta.Grind.Arith.Cutsat.propagateLe (e : Expr) (eqTrue : Bool) :
                  GoalM Unit
                  Instances For
                    source
                    def Lean.Meta.Grind.Arith.Cutsat.propagateLt (e : Expr) (eqTrue : Bool) :
                    GoalM Unit
                    Instances For