chore: fix error in Grind/Arith/Linear/StructId

2026-03-17 18:34:06 +00:00 · 2025-08-24 18:19:34 +10:00
1 changed files with 2 additions and 2 deletions
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean
@@ -245,11 +245,11 @@ where
    let rec getHSMulFn? : GoalM (Option Expr) := do
      let smulType := mkApp3 (mkConst ``HSMul [0, u, u]) Int.mkType type type
      let some smulInst ← synthInstance? smulType | return none
-      internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Int.mkType type smulInst smulInst
+      internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Int.mkType type type smulInst
    let rec getHSMulNatFn? : GoalM (Option Expr) := do
      let smulType := mkApp3 (mkConst ``HSMul [0, u, u]) Nat.mkType type type
      let some smulInst ← synthInstance? smulType | return none
-      internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Nat.mkType type smulInst smulInst
+      internalizeFn <| mkApp4 (mkConst ``HSMul.hSMul [0, u, u]) Nat.mkType type type smulInst
    let zsmulFn? ← getHSMulFn?
    let nsmulFn? ← getHSMulNatFn?
    let homomulFn? ← if commRingInst?.isSome then