def Lean.Meta.Grind.Arith.Linear.isAddInst (struct : Struct) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.Linear.isZeroInst (struct : Struct) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.Linear.isSMulIntInst (struct : Struct) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.Linear.isSMulNatInst (struct : Struct) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.Linear.isHomoMulInst (struct : Struct) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.Linear.isHSMulIntInst (struct : Struct) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.Linear.isHSMulNatInst (struct : Struct) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.Linear.isSubInst (struct : Struct) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.Linear.isNegInst (struct : Struct) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.Linear.reportInstIssue (e : Expr) : GoalM Unit

def Lean.Meta.Grind.Arith.Linear.reify? (e : Expr) (skipVar : Bool) (generation : Nat := 0) : LinearM (Option LinExpr)

Converts a Lean IntModule expression e into a LinExpr

If skipVar is true, then the result is none if e is not an interpreted IntModule term. We use skipVar := false when processing inequalities, and skipVar := true for equalities and disequalities