test for issue #23

lecopivo · Sep 16, 2023 · 78575ce · 78575ce
1 parent 5834e79
commit 78575ce
Showing 1 changed file with 22 additions and 0 deletions.
diff --git a/test/issues/23.lean b/test/issues/23.lean
@@ -0,0 +1,22 @@
+import SciLean
+
+open SciLean
+
+variable 
+  {K : Type _} [IsROrC K]
+  {X : Type _} [Vec K X]
+
+-- example (f : X → Fin 5 → Fin 10 → Fin 15→ K) (hf : ∀ i j k, IsDifferentiable K (f · i j k))
+--   : IsDifferentiable K f := by fprop
+
+-- example (f : X → Fin 5 → Fin 10 → Fin 15→ K) (hf : ∀ i j k, IsDifferentiable K (f · i j k))
+--   : IsDifferentiable K (fun x => f x i j) := by fprop
+
+-- example (f : X → Fin 5 → Fin 10 → Fin 15→ K) (hf : ∀ i j k, IsDifferentiable K (f · i j k))
+--   : IsDifferentiable K (fun x => f x) := by fprop
+
+-- example (f : X → Fin 5 → Fin 10 → Fin 15→ K) (hf : ∀ i j k, IsDifferentiable K (f · i j k))
+--   : IsDifferentiable K (fun x i j => f x i j) := by fprop
+
+example (f : X → Fin 5 → Fin 10 → Fin 15→ K) (hf : ∀ i j k, IsDifferentiable K (f · i j k))
+  : IsDifferentiable K (fun x i j k => f x i j k) := by fprop