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.isHMulIntInst (struct : Struct) (inst : Expr) : Bool

def Lean.Meta.Grind.Arith.Linear.isHMulNatInst (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) : 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

def Lean.Meta.Grind.Arith.Linear.reify?.toVar (e : Expr) : LinearM LinExpr

def Lean.Meta.Grind.Arith.Linear.reify?.asVar (e : Expr) : LinearM LinExpr

def Lean.Meta.Grind.Arith.Linear.reify?.asTopVar (skipVar : Bool) (e : Expr) : LinearM (Option LinExpr)

def Lean.Meta.Grind.Arith.Linear.reify?.isOfNatZero (e : Expr) : LinearM Bool

partial def Lean.Meta.Grind.Arith.Linear.reify?.processHMul (i a b : Expr) : LinearM (Option LinExpr)

partial def Lean.Meta.Grind.Arith.Linear.reify?.processHSMul (i a b : Expr) : LinearM (Option LinExpr)

partial def Lean.Meta.Grind.Arith.Linear.reify?.go (e : Expr) : LinearM LinExpr