def Lean.Meta.Simp.Arith.withAbstractAtoms (atoms : Array Expr) (type : Name) (k : Array Expr → MetaM (Option (Expr × Expr))) : MetaM (Option (Expr × Expr))

Equations

• Lean.Meta.Simp.Arith.withAbstractAtoms atoms type k = Lean.Meta.Simp.Arith.withAbstractAtoms.go atoms k (Lean.mkConst type) 0 #[] #[] #[]

@[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

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

def Lean.Meta.Simp.Arith.isLinearTerm (e : Expr) (isNatExpr : Bool) : Bool

Quick filter for linear terms.

Equations

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

partial def Lean.Meta.Simp.Arith.isLinearCnstr (e : Expr) : Bool

Quick filter for linear constraints.

def Lean.Meta.Simp.Arith.isDvdCnstr (e : Expr) : Bool

Equations

• Lean.Meta.Simp.Arith.isDvdCnstr e = e.isAppOfArity `Dvd.dvd 4