Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.Inv

source
def Int.Linear.Poly.checkCoeffs :
Poly → Bool

Returns true if all coefficients are not 0.

Equations
    Instances For
      source
      def Int.Linear.Poly.checkNoElimVars (p : Poly) :
      Lean.Meta.Grind.GoalM Unit
      Equations
        Instances For
          source
          def Int.Linear.Poly.checkOccs (p : Poly) :
          Lean.Meta.Grind.GoalM Unit
          Equations
            Instances For
              source
              def Int.Linear.Poly.checkOccs.go (y : Var) (p : Poly) :
              Lean.Meta.Grind.GoalM Unit
              Equations
                Instances For
                  source
                  def Int.Linear.Poly.checkCnstrOf (p : Poly) (x : Var) :
                  Lean.Meta.Grind.GoalM Unit
                  Equations
                    Instances For
                      source
                      def Lean.Meta.Grind.Arith.Cutsat.checkLeCnstrs (css : PArray (PArray LeCnstr)) (isLower : Bool) :
                      GoalM Unit
                      Equations
                        Instances For
                          source
                          def Lean.Meta.Grind.Arith.Cutsat.checkLowers :
                          GoalM Unit
                          Equations
                            Instances For
                              source
                              def Lean.Meta.Grind.Arith.Cutsat.checkUppers :
                              GoalM Unit
                              Equations
                                Instances For
                                  source
                                  def Lean.Meta.Grind.Arith.Cutsat.checkDvds :
                                  GoalM Unit
                                  Equations
                                    Instances For
                                      source
                                      def Lean.Meta.Grind.Arith.Cutsat.checkVars :
                                      GoalM Unit
                                      Equations
                                        Instances For
                                          source
                                          def Lean.Meta.Grind.Arith.Cutsat.checkElimEqs :
                                          GoalM Unit
                                          Equations
                                            Instances For
                                              source
                                              def Lean.Meta.Grind.Arith.Cutsat.checkElimStack :
                                              GoalM Unit
                                              Equations
                                                Instances For
                                                  source
                                                  def Lean.Meta.Grind.Arith.Cutsat.checkDiseqCnstrs :
                                                  GoalM Unit
                                                  Equations
                                                    Instances For
                                                      source
                                                      def Lean.Meta.Grind.Arith.Cutsat.checkInvariants :
                                                      GoalM Unit
                                                      Equations
                                                        Instances For