Documentation

Lean.Meta.Tactic.Grind.Arith.Util

Returns true if e is of the form Nat

Equations
Instances For

    Returns true if e is of the form Int

    Equations
    Instances For

      Returns true if e is of the form @instHAdd Nat instAddNat

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Returns true if e is instLENat

        Equations
        Instances For

          Returns some (a, b) if e is of the form

          @HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) a b
          
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Returns true if e is of the form

            @HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) _ _
            
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Returns some k if e @OfNat.ofNat Nat _ (instOfNatNat k)

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Quote e using and if e is an arithmetic term that is being treated as a variable.

                  Equations
                  Instances For

                    gcdExt a b returns the triple (g, α, β) such that

                    • g = gcd a b (with g ≥ 0), and
                    • g = α * a + β * b.

                    Helper monad for collecting decision variables in linarith and cutsat

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[reducible, inline]
                      Equations
                      Instances For

                        Return auxiliary expression used as "virtual" parent when internalizing auxiliary expressions created by toIntModuleExpr. The function toIntModuleExpr converts a CommRing polynomial into a IntModule expression. We don't want this auxiliary expression to be internalized by the CommRing module since it uses a nonstandard encoding with @HMul.hMul Int α α, a virtual One.one constant, etc.

                        Equations
                        Instances For
                          def Lean.Meta.Grind.Arith.getIsCharInst? (u : Level) (type semiringInst : Expr) :
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[specialize #[]]
                              def Lean.Meta.Grind.Arith.split {α : Type u_1} (cs : PArray α) (getCoeff : αInt) :
                              PArray α × Array (Int × α)
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For