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

Equations

• Lean.Meta.Grind.Arith.Linear.isAddInst struct inst = Lean.Meta.Grind.isSameExpr struct.addFn.appArg! inst

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

Equations

• Lean.Meta.Grind.Arith.Linear.isZeroInst struct inst = Lean.Meta.Grind.isSameExpr struct.zero.appArg! inst

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

Equations

• Lean.Meta.Grind.Arith.Linear.isSMulIntInst struct inst = Lean.Meta.Grind.isSameExpr struct.zsmulFn.appArg! inst

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

Equations

• Lean.Meta.Grind.Arith.Linear.isSMulNatInst struct inst = Lean.Meta.Grind.isSameExpr struct.nsmulFn.appArg! inst

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

Equations

• Lean.Meta.Grind.Arith.Linear.isHomoMulInst struct inst = match struct.homomulFn? with | some homomulFn => Lean.Meta.Grind.isSameExpr homomulFn inst | x => false

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

Equations

• Lean.Meta.Grind.Arith.Linear.isHSMulIntInst struct inst = match struct.zsmulFn? with | some smulFn => Lean.Meta.Grind.isSameExpr smulFn.appArg! inst | x => false

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

Equations

• Lean.Meta.Grind.Arith.Linear.isHSMulNatInst struct inst = match struct.nsmulFn? with | some smulFn => Lean.Meta.Grind.isSameExpr smulFn.appArg! inst | x => false

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

Equations

• Lean.Meta.Grind.Arith.Linear.isSubInst struct inst = Lean.Meta.Grind.isSameExpr struct.subFn.appArg! inst

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

Equations

• Lean.Meta.Grind.Arith.Linear.isNegInst struct inst = Lean.Meta.Grind.isSameExpr struct.negFn.appArg! inst

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

Equations

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

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

Equations

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