Documentation

Lean.Meta.Tactic.Simp.Arith.Util

source
def Lean.Meta.Simp.Arith.isLinearTerm? (e : Expr) :
Option Expr

Quick filter for linear terms.

Equations
    Instances For
      source
      def Lean.Meta.Simp.Arith.isLinearTerm (e : Expr) :
      Bool
      Equations
        Instances For
          source
          def Lean.Meta.Simp.Arith.isLinearPosCnstr (e : Expr) :
          Bool
          Equations
            Instances For
              source
              def Lean.Meta.Simp.Arith.isLinearCnstr (e : Expr) :
              Bool
              Equations
                Instances For
                  source
                  def Lean.Meta.Simp.Arith.isDvdCnstr (e : Expr) :
                  Bool
                  Equations
                    Instances For