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 #[] #[] #[]

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

Quick filter for linear terms.

Equations

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

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

Equations

• Lean.Meta.Simp.Arith.isLinearTerm e = (Lean.Meta.Simp.Arith.isLinearTerm? e).isSome

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

Equations

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

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

Equations

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

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

Equations

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