extra example for basic gradients

lecopivo · Sep 4, 2023 · 92ca574 · 92ca574
1 parent 9a832a7
commit 92ca574
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/test/basic_gradients.lean b/test/basic_gradients.lean
@@ -68,6 +68,13 @@ example
 by 
   (conv => lhs; autodiff)
 
+example
+  : (∇ (x : K ^ Idx 10), ∑ i, x[i])
+    =
+    fun x => ⊞ i => (1:K) :=
+by 
+  (conv => lhs; autodiff)
+
 example
   : (∇ (x : Fin 10 → K), ∑ i, ‖x i‖₂²)
     =
@@ -82,4 +89,3 @@ example (A : Fin 5 → Fin 10 → K)
 by 
   (conv => lhs; autodiff)
 
-