Documentation

Lean.Meta.Tactic.Grind.Arith.Linear.Inv

source
def Lean.Grind.Linarith.Poly.isSorted (p : Poly) :
Bool

Returns true if the variables in the given polynomial are sorted in decreasing order.

Equations
    Instances For
      source
      def Lean.Grind.Linarith.Poly.isSorted.go :
      Option Var → Poly → Bool
      Equations
        Instances For
          source
          def Lean.Grind.Linarith.Poly.checkCoeffs :
          Poly → Bool

          Returns true if all coefficients are not 0.

          Equations
            Instances For
              source
              def Lean.Grind.Linarith.Poly.checkOccs (p : Poly) :
              Meta.Grind.Arith.Linear.LinearM Unit
              Equations
                Instances For
                  source
                  def Lean.Grind.Linarith.Poly.checkOccs.go (y : Var) (p : Poly) :
                  Meta.Grind.Arith.Linear.LinearM Unit
                  Equations
                    Instances For
                      source
                      def Lean.Grind.Linarith.Poly.checkNoElimVars (p : Poly) :
                      Meta.Grind.Arith.Linear.LinearM Unit
                      Equations
                        Instances For
                          source
                          def Lean.Grind.Linarith.Poly.checkCnstrOf (p : Poly) (x : Var) :
                          Meta.Grind.Arith.Linear.LinearM Unit
                          Equations
                            Instances For
                              source
                              def Lean.Meta.Grind.Arith.Linear.checkLeCnstrs (css : PArray (PArray IneqCnstr)) (isLower : Bool) :
                              LinearM Unit
                              Equations
                                Instances For
                                  source
                                  def Lean.Meta.Grind.Arith.Linear.checkLowers :
                                  LinearM Unit
                                  Equations
                                    Instances For
                                      source
                                      def Lean.Meta.Grind.Arith.Linear.checkUppers :
                                      LinearM Unit
                                      Equations
                                        Instances For
                                          source
                                          def Lean.Meta.Grind.Arith.Linear.checkDiseqCnstrs :
                                          LinearM Unit
                                          Equations
                                            Instances For
                                              source
                                              def Lean.Meta.Grind.Arith.Linear.checkVars :
                                              LinearM Unit
                                              Equations
                                                Instances For
                                                  source
                                                  def Lean.Meta.Grind.Arith.Linear.checkStructInvs :
                                                  LinearM Unit
                                                  Equations
                                                    Instances For
                                                      source
                                                      def Lean.Meta.Grind.Arith.Linear.checkInvariants :
                                                      GoalM Unit
                                                      Equations
                                                        Instances For