fix comment

lecopivo · Oct 18, 2024 · 66ee02b · 66ee02b
1 parent e7bcdb0
commit 66ee02b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/SciLean/Modules/ML/XLA/ConvWithPaddingStride.lean b/SciLean/Modules/ML/XLA/ConvWithPaddingStride.lean
@@ -221,7 +221,7 @@ theorem convWithPaddingStride.arg_x.adjoint_rule
       if h : (0 ≤ di' ∧ di' < outDim) ∧ (ri' = 0) then
         have := h.1
         z[di'] * x[k] * y[j]
-      else 0 := by sorry -- swap sums and rewrite the condition in terms of `i'`
+      else 0 := by sorry -- remove sum over `i`
 
     _ = ∑ (k : TensorIndex spDims), ∑ (j : TensorIndex kerDims),
       let i' := k.1 * xdil + j.1 * ydil - ((kerDims - 1) * ydil - low)