# HG changeset patch
# User haftmann
# Date 1552553164 -3600
# Node ID 1bd74a0944b3d0f0c5f4bf80ee7e56e5894aeec7
# Parent  4343c1bfa52d63a9a9a2d50361005e27bc129893
slightly more complete check of code generation for immutable arrays

diff -r 4343c1bfa52d -r 1bd74a0944b3 src/HOL/ex/IArray_Examples.thy
--- a/src/HOL/ex/IArray_Examples.thy	Wed Mar 13 20:44:39 2019 +0100
+++ b/src/HOL/ex/IArray_Examples.thy	Thu Mar 14 09:46:04 2019 +0100
@@ -29,5 +29,13 @@
 lemma "sum (IArray [1,2,3,4,5,6,7,8,9::int]) = 45"
 by eval
 
+definition partial_geometric_sum :: "'a::comm_ring_1 list \<Rightarrow> 'a"
+  where "partial_geometric_sum xs = (let
+    values = IArray xs;
+    coefficients = IArray.of_fun of_nat (length xs)
+  in sum_list (map (\<lambda>i. values !! i * coefficients !! i) [0..<IArray.length values]))"
+
+export_code partial_geometric_sum checking SML OCaml? Haskell? Scala
+
 end