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.

Instances For
    source
    def Int.Linear.Poly.getGeneration (p : Poly) :
    Lean.Meta.Grind.GoalM Nat
    Instances For
      source
      def Lean.Meta.Grind.Arith.Cutsat.getIntRingId? :
      GoalM (Option Nat)
      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

        Instances For