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

Instances For

source
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.

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For