Documentation

Lean.Meta.Tactic.Simp.Arith.Util

source
def Lean.Meta.Simp.Arith.withAbstractAtoms (atoms : Array Expr) (type : Name) (k : Array Expr → MetaM (Option (Expr × Expr))) :
MetaM (Option (Expr × Expr))
Equations
    Instances For
      source
      @[irreducible]
      def Lean.Meta.Simp.Arith.withAbstractAtoms.go (atoms : Array Expr) (k : Array Expr → MetaM (Option (Expr × Expr))) (type : Expr) (i : Nat) (atoms' xs args : Array Expr) :
      MetaM (Option (Expr × Expr))
      Equations
        Instances For
          source
          def Lean.Meta.Simp.Arith.isLinearTerm (e : Expr) (isNatExpr : Bool) :
          Bool

          Quick filter for linear terms.

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

              Quick filter for linear constraints.

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