def Lean.Meta.Linear.isLinearTerm (e : Expr) : Bool

Quick filter for linear terms.

Equations

• Lean.Meta.Linear.isLinearTerm e = if (!e.getAppFn.isConst) = true then false else let n := e.getAppFn.constName!; n == `HAdd.hAdd || n == `HMul.hMul || n == `HSub.hSub || n == `Nat.succ

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

Quick filter for linear constraints.