Documentation

Lean.Meta.Tactic.Simp.Arith.Util

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

Quick filter for linear terms.

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