Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing

CommRing interface for cutsat. We use it to normalize nonlinear polynomials.

source
def Int.Linear.Poly.isNonlinear (p : Poly) :
Lean.Meta.Grind.GoalM Bool

Returns true if p contains a nonlinear monomial.

Equations
    Instances For
      source
      def Int.Linear.Poly.getGeneration (p : Poly) :
      Lean.Meta.Grind.GoalM Nat
      Equations
        Instances For
          source
          def Int.Linear.Poly.getGeneration.go :
          Poly → Nat → Lean.Meta.Grind.GoalM Nat
          Equations
            Instances For
              source
              def Lean.Meta.Grind.Arith.Cutsat.getIntRingId? :
              GoalM (Option Nat)
              Equations
                Instances For
                  source
                  def Int.Linear.Poly.normCommRing? (p : Poly) :
                  Lean.Meta.Grind.GoalM (Option (Lean.Meta.Grind.Arith.CommRing.RingExpr × Lean.Grind.CommRing.Poly × Poly))

                  Normalize the polynomial using CommRing

                  Equations
                    Instances For