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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.Grind.Arith.Linear.reify?.toVar e = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.mkVar e pure (Lean.Grind.Linarith.Expr.var __do_lift)

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.Grind.Arith.Linear.reify?.isOfNatZero e = do let __do_lift ← Lean.Meta.Grind.Arith.Linear.getStruct Lean.Meta.withDefault (liftM (Lean.Meta.isDefEq e __do_lift.ofNatZero))

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