diff --git a/.charon_version b/.charon_version
new file mode 100644
index 00000000..2c88ab23
--- /dev/null
+++ b/.charon_version
@@ -0,0 +1 @@
+0.1.123
diff --git a/bin/main.ml b/bin/main.ml
index b8cf5d72..5cefa28c 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -256,7 +256,7 @@ Supported options:|}
   let files = Krml.Inlining.drop_unused files in
   let files = Eurydice.Cleanup2.remove_array_temporaries#visit_files () files in
   Eurydice.Logging.log "Phase2.25" "%a" pfiles files;
-  let files = Eurydice.Cleanup2.remove_array_repeats#visit_files () files in
+  let files = Eurydice.Cleanup2.remove_array_repeats#visit_files false files in
   Eurydice.Logging.log "Phase2.26" "%a" pfiles files;
   let files = Eurydice.Cleanup2.rewrite_slice_to_array#visit_files () files in
   let ((map, _, _) as map3), files = Krml.DataTypes.everything files in
@@ -313,6 +313,7 @@ Supported options:|}
   Eurydice.Cleanup3.(also_skip_prefix_for_external_types scope_env)#visit_files () files;
   let files = Eurydice.Cleanup3.decay_cg_externals#visit_files (scope_env, false) files in
   let files = Eurydice.Cleanup3.add_extra_type_to_slice_index#visit_files () files in
+  let files = Eurydice.Cleanup3.remove_builtin_decls files in  
   Eurydice.Logging.log "Phase3.1" "%a" pfiles files;
   let c_name_map = Krml.GlobalNames.mapping (fst scope_env) in
 
diff --git a/include/eurydice_glue.h b/include/eurydice_glue.h
index 04b84367..5f1b28fe 100644
--- a/include/eurydice_glue.h
+++ b/include/eurydice_glue.h
@@ -169,10 +169,11 @@ typedef struct {
 // Distinguished support for some PartialEq trait implementations
 //
 // core::cmp::PartialEq<@Array<U, N>> for @Array<T, N>
-#define Eurydice_array_eq(sz, a1, a2, t) (memcmp(a1, a2, sz * sizeof(t)) == 0)
+#define Eurydice_array_eq(sz, a1, a2, t)                                       \
+  (memcmp((a1)->data, (a2)->data, sz * sizeof(t)) == 0)
 // core::cmp::PartialEq<&0 (@Slice<U>)> for @Array<T, N>
 #define Eurydice_array_eq_slice(sz, a1, s2, t, _)                              \
-  (memcmp(a1, (s2)->ptr, sz * sizeof(t)) == 0)
+  (memcmp((a1)->data, (s2)->ptr, sz * sizeof(t)) == 0)
 
 // DEPRECATED -- should no longer be generated
 #define core_array_equality__core__cmp__PartialEq__Array_U__N___for__Array_T__N___eq( \
@@ -264,30 +265,43 @@ typedef char Eurydice_derefed_slice[];
 extern "C" {
 #endif
 
-static inline uint16_t core_num__u16__from_le_bytes(uint8_t buf[2]) {
-  return load16_le(buf);
+
+typedef struct Eurydice_arr_8b_s { uint8_t data[2]; } Eurydice_arr_8b;
+typedef struct Eurydice_arr_e9_s { uint8_t data[4]; } Eurydice_arr_e9;
+typedef struct Eurydice_arr_c4_s { uint8_t data[8]; } Eurydice_arr_c4;
+  
+
+  
+static inline uint16_t core_num__u16__from_le_bytes(Eurydice_arr_8b buf) {
+  return load16_le(buf.data);
 }
 
-static inline void core_num__u32__to_be_bytes(uint32_t src, uint8_t dst[4]) {
+static inline Eurydice_arr_e9 core_num__u32__to_be_bytes(uint32_t src) {
   // TODO: why not store32_be?
+  Eurydice_arr_e9 a;
   uint32_t x = htobe32(src);
-  memcpy(dst, &x, 4);
+  memcpy(a.data, &x, 4);
+  return a;
 }
 
-static inline void core_num__u32__to_le_bytes(uint32_t src, uint8_t dst[4]) {
-  store32_le(dst, src);
+static inline Eurydice_arr_e9 core_num__u32__to_le_bytes(uint32_t src) {
+  Eurydice_arr_e9 a;
+  store32_le(a.data,src);
+  return a;
 }
 
-static inline uint32_t core_num__u32__from_le_bytes(uint8_t buf[4]) {
-  return load32_le(buf);
+static inline uint32_t core_num__u32__from_le_bytes(Eurydice_arr_e9 buf) {
+  return load32_le(buf.data);
 }
 
-static inline void core_num__u64__to_le_bytes(uint64_t v, uint8_t buf[8]) {
-  store64_le(buf, v);
+static inline Eurydice_arr_c4 core_num__u64__to_le_bytes(uint64_t v) {
+  Eurydice_arr_c4 a;
+  store64_le(a.data, v);
+  return a;
 }
 
-static inline uint64_t core_num__u64__from_le_bytes(uint8_t buf[8]) {
-  return load64_le(buf);
+static inline uint64_t core_num__u64__from_le_bytes(Eurydice_arr_c4 buf) {
+  return load64_le(buf.data);
 }
 
 static inline int64_t
@@ -553,6 +567,10 @@ static inline char *malloc_and_init(size_t sz, char *init) {
 #define Eurydice_box_new(init, t, t_dst)                                       \
   ((t_dst)(malloc_and_init(sizeof(t), (char *)(&init))))
 
+// Initializer for array of size zero
+#define Eurydice_empty_array(dummy, t, t_dst)                                  \
+  ((t_dst) { .data = { } })
+
 #define Eurydice_box_new_array(len, ptr, t, t_dst)                             \
   ((t_dst)(malloc_and_init(len * sizeof(t), (char *)(ptr))))
 
diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml
index c1ee131a..4ce50ef8 100644
--- a/lib/AstOfLlbc.ml
+++ b/lib/AstOfLlbc.ml
@@ -383,6 +383,8 @@ let lookup_field env typ_id field_id =
   let field = List.nth fields i in
   ensure_named i field.field_name
 
+let expression_of_struct_Arr (expr_array : K.expr) = K.EFlat [(Some "data", expr_array)]
+
 let rec pre_typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ =
   match ty with
   | TVar var -> K.TBound (lookup_typ env (C.expect_free_var var))
@@ -400,15 +402,6 @@ let rec pre_typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ =
       (* We compile slices to fat pointers, which hold the pointer underneath -- no need for an
          extra reference here. *)
       Builtin.mk_slice (typ_of_ty env t)
-  | TAdt
-      {
-        id = TBuiltin TBox;
-        generics = { types = [ TAdt { id = TBuiltin TArray; generics = { types = [ t ]; _ } } ]; _ };
-      }
-  | TRef (_, TAdt { id = TBuiltin TArray; generics = { types = [ t ]; _ } }, _) ->
-      (* We collapse Ref(Array) into a pointer type, leveraging C's implicit decay between array
-         types and pointer types. *)
-      K.TBuf (typ_of_ty env t, false)
   | TRef (_, TAdt { id = TBuiltin TStr; generics = { types = []; _ } }, _) -> Builtin.str_t
   | TRef (_, t, _) ->
       (* Normal reference *)
@@ -427,7 +420,7 @@ let rec pre_typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ =
         | _ -> TTuple (List.map (typ_of_ty env) args)
       end
   | TAdt { id = TBuiltin TArray; generics = { types = [ t ]; const_generics = [ cg ]; _ } } ->
-      maybe_cg_array env t cg
+     typ_of_struct_arr env t cg
   | TAdt { id = TBuiltin TSlice; generics = { types = [ t ]; _ } } ->
       (* Appears in instantiations of patterns and generics, so we translate it to a placeholder. *)
       TApp (Builtin.derefed_slice, [ typ_of_ty env t ])
@@ -480,7 +473,12 @@ and typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ =
          from this to the DST above. *)
       t
 
-and maybe_cg_array env t cg =
+and typ_of_struct_arr (env: env) (t: C.ty) (cg: C.const_generic) : K.typ =
+  let typ_t = typ_of_ty env t in
+  let cg = cg_of_const_generic env cg in
+  Builtin.mk_arr typ_t cg
+  
+let maybe_cg_array (env : env) (t : C.ty) (cg : C.const_generic) =
   match cg with
   | CgValue _ -> K.TArray (typ_of_ty env t, constant_of_scalar_value (assert_cg_scalar cg))
   | CgVar var ->
@@ -489,15 +487,6 @@ and maybe_cg_array env t cg =
       K.TCgArray (typ_of_ty env t, id)
   | _ -> failwith "TODO: CgGlobal"
 
-(* Helpers: expressions *)
-
-(* To be desugared later into variable hoisting, allocating suitable storage space, followed by a
-   memcpy -- this is just a placeholder and isn't even type-checked. *)
-let mk_deep_copy (e : K.expr) (l : K.expr) =
-  let builtin_copy_operator = K.EQualified Builtin.array_copy in
-  let builtin_copy_operator_t = K.TArrow (TAny, TAny) in
-  K.(with_type TAny (EApp (with_type builtin_copy_operator_t builtin_copy_operator, [ e; l ])))
-
 (* Environment: expressions *)
 
 let is_var v2 v1 =
@@ -705,10 +694,6 @@ let rec expression_of_place (env : env) (p : C.place) : K.expr =
       (* L.log "AstOfLlbc" "e=%a\nty=%s\npe=%s\n" pexpr sub_e (C.show_ty sub_place.ty) *)
       (*   (C.show_projection_elem pe); *)
       match pe, sub_place, sub_place.ty with
-      | C.Deref, _, TRef (_, TAdt { id = TBuiltin TArray; generics = { types = [ t ]; _ } }, _)
-      | C.Deref, _, TRawPtr (TAdt { id = TBuiltin TArray; generics = { types = [ t ]; _ } }, _) ->
-          (* Array is passed by reference; when appearing in a place, it'll automatically decay in C *)
-          K.with_type (TBuf (typ_of_ty env t, false)) !*sub_e.K.node
       | C.Deref, _, TRef (_, TAdt { id = TBuiltin TSlice; _ }, _)
       | C.Deref, _, TRawPtr (TAdt { id = TBuiltin TSlice; _ }, _) -> !*sub_e
       | ( C.Deref,
@@ -717,7 +702,8 @@ let rec expression_of_place (env : env) (p : C.place) : K.expr =
           (* All types represented as a pointer at run-time, compiled to a C pointer *)
           begin
             match !*sub_e.K.typ with
-            | TBuf (t_pointee, _) | TArray (t_pointee, _) ->
+            | TArray (_, _) -> assert false
+            | TBuf (t_pointee, _) -> 
                 Krml.Helpers.(mk_deref t_pointee !*sub_e.K.node)
             | t ->
                 L.log "AstOfLlbc" "UNHANDLED DEREFERENCE\ne=%a\nt=%a\nty=%s\npe=%s\n" pexpr !*sub_e
@@ -969,7 +955,7 @@ let mk_op_app (op : K.op) (first : K.expr) (rest : K.expr list) : K.expr =
 let maybe_addrof (_env : env) (ty : C.ty) (e : K.expr) =
   (* ty is the *original* Rust type *)
   match ty with
-  | TAdt { id = TBuiltin (TArray | TSlice); _ } -> e
+  | TAdt { id = TBuiltin (TSlice); _ } -> e
   | _ -> K.(with_type (TBuf (e.typ, false)) (EAddrOf e))
 
 (** Handling trait clauses as dictionaries *)
@@ -1589,14 +1575,7 @@ let expression_of_operand (env : env) (op : C.operand) : K.expr =
   | Copy ({ kind = PlaceGlobal { id; _ }; _ } as p) when global_is_const env id ->
       (* No need to copy a const since by definition it cannot be modified *)
       expression_of_place env p
-  | Copy p ->
-      let e = expression_of_place env p in
-      begin
-        match p.ty with
-        | C.TAdt { id = TBuiltin TArray; generics = { const_generics = [ cg ]; _ } } ->
-            mk_deep_copy e (expression_of_const_generic env cg)
-        | _ -> e
-      end
+  | Copy p -> expression_of_place env p
   | Move p -> expression_of_place env p
   | Constant { value = CLiteral l; _ } -> expression_of_literal env l
   | Constant { value = CVar var; _ } -> expression_of_cg_var_id env (C.expect_free_var var)
@@ -1640,6 +1619,13 @@ let is_box_place (p : C.place) =
   | C.TAdt { id = TBuiltin TBox; _ } -> true
   | _ -> false
 
+let expression_of_cg (env : env) (cg : K.cg) =
+  match cg with
+  |CgConst n -> Krml.Helpers.mk_sizet (int_of_string (snd n))
+  |CgVar var ->
+    let diff = List.length env.binders - List.length env.cg_binders in
+    K.with_type (K.TInt SizeT) (K.EBound (var + diff))
+
 let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr =
   match p with
   | Use op -> expression_of_operand env op
@@ -1737,63 +1723,27 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr =
       let t_from = typ_of_ty env ty_from and t_to = typ_of_ty env ty_to in
       let e = expression_of_operand env e in
       begin
-        (* TODO: this whole piece of code should handle TCgArray too *)
-        match t_from, is_dst env t_to, ty_from, ty_to with
-        | TBuf (TApp (lid1, [ TArray (u1, n) ]), _), Some (lid2, TApp (slice_hd, [ u2 ]), t_u), _, _
-          when lid1 = lid2 && u1 = u2 && slice_hd = Builtin.derefed_slice ->
-            let len = Krml.Helpers.mk_sizet (int_of_string (snd n)) in
+        match t_from, is_dst env t_to with
+        | TBuf (TApp (lid1, [ K.TCgApp (K.TApp (lid_arr, [ u1 ]), cg) ]) , _), Some (lid2, TApp (slice_hd, [ u2 ]), t_u)
+          when lid1 = lid2 && u1 = u2 && slice_hd = Builtin.derefed_slice && lid_arr = Builtin.arr ->
             (* Cast from a struct whose last field is `t data[n]` to a struct whose last field is
              `Eurydice_derefed_slice data` (a.k.a. `char data[]`) *)
+            let len = expression_of_cg env cg in
             let ptr = K.with_type (TBuf (t_u, false)) (K.ECast (e, TBuf (t_u, false))) in
             Builtin.dst_new ~len ~ptr t_u
-        | ( _,
-            _,
-            TAdt
-              {
-                id = TBuiltin TBox;
-                generics =
-                  {
-                    types =
-                      [
-                        TAdt
-                          {
-                            id = TBuiltin TArray;
-                            generics = { types = [ t1 ]; const_generics = [ cg ]; _ };
-                          };
-                      ];
-                    _;
-                  };
-              },
-            TAdt
-              {
-                id = TBuiltin TBox;
-                generics =
-                  { types = [ TAdt { id = TBuiltin TSlice; generics = { types = [ t2 ]; _ } } ]; _ };
-              } ) ->
-            (* Cast from Box<[T; N]> to Box<[T]> which we represent as Eurydice_slice.
-               This is basically the same as above, but because we translate Box straight to *, in
-               order to account for array decay and the like, we have to match on original Rust
-               types. Note that we cannot really compile Box<T> to a struct, as it would defeat the
-               pointer semantics of Box and turn passing by reference into passing by value (array
-               within struct).
-            *)
-            assert (t1 = t2);
-            let t_from = maybe_cg_array env t1 cg in
-            let t, n =
-              match t_from with
-              | TArray (t, n) -> t, n
-              | _ -> failwith "impossible"
-            in
-            let len = Krml.Helpers.mk_sizet (int_of_string (snd n)) in
-            (* slice_of_boxed_array: 0* -> size_t -> Eurydice_slice 0 *)
-            let slice_of_boxed_array = Builtin.(expr_of_builtin slice_of_boxed_array) in
-            (* slice_of_boxed_array: 0* -> size_t -> Eurydice_slice 0 *)
-            let slice_of_boxed_array =
+        | TBuf ( K.TCgApp (K.TApp (lid_arr, [ t ]), cg), _), _
+          when lid_arr = Builtin.arr ->
+            (* Cast from Box<[T;N]> to Box<[T]> which we represent as Eurydice_slice *)
+            let len = expression_of_cg env cg in
+            (* array_to_slice: size_t -> arr -> Eurydice_slice 0 *)
+            let array_to_slice = Builtin.(expr_of_builtin array_to_slice) in
+            let diff = List.length env.binders - List.length env.cg_binders in
+            let array_to_slice =
               K.with_type
-                (Krml.DeBruijn.subst_t t 0 slice_of_boxed_array.typ)
-                (K.ETApp (slice_of_boxed_array, [], [], [ t ]))
+                (Krml.DeBruijn.(subst_t t 0 (subst_ct diff len 0 (Builtin.array_to_slice.typ))))
+                (K.ETApp (array_to_slice, [ len ], [], [ t ]))
             in
-            K.(with_type (Builtin.mk_slice t) (EApp (slice_of_boxed_array, [ e; len ])))
+            K.(with_type (Builtin.mk_slice t) (EApp (array_to_slice, [ e ])))
         | _ ->
             Krml.Warn.fatal_error "unknown unsize cast: `%s`\nt_to=%a\nt_from=%a"
               (Charon.PrintExpressions.cast_kind_to_string env.format_env ck)
@@ -1872,9 +1822,24 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr =
   | Aggregate (AggregatedAdt ({ id = TBuiltin _; _ }, _, _), _) ->
       failwith "unsupported: AggregatedAdt / TAssume"
   | Aggregate (AggregatedArray (t, cg), ops) ->
-      K.with_type
-        (TArray (typ_of_ty env t, constant_of_scalar_value (assert_cg_scalar cg)))
-        (K.EBufCreateL (Stack, List.map (expression_of_operand env) ops))
+     let ty = typ_of_ty env t in
+     let typ_arr = typ_of_struct_arr env t cg in
+     begin
+       match ops with
+       | [] ->
+          let empty_array =
+            K.with_type
+              (Krml.DeBruijn.(subst_t ty 0 (Builtin.empty_array.typ)))
+              (K.ETApp (Builtin.(expr_of_builtin empty_array), [], [], [ ty ]))
+          in
+          K.with_type typ_arr (K.EApp (empty_array, [ K.with_type ty K.EAny ]))
+          (* a dummy arg is needed to pass the checker *)
+       | _ ->
+           let array_expr = K.with_type
+             (TArray (typ_of_ty env t, constant_of_scalar_value (assert_cg_scalar cg)))
+             (K.EBufCreateL (Stack, List.map (expression_of_operand env) ops)) in
+           K.with_type typ_arr (expression_of_struct_Arr array_expr)
+     end 
   | rvalue ->
       failwith
         ("unsupported rvalue: `"
@@ -1991,6 +1956,7 @@ and expression_of_statement_kind (env : env) (ret_var : C.local_id) (s : C.state
       (* Special treatment *)
       let e = expression_of_operand env e in
       let t = typ_of_ty env ty in
+      let t_array = maybe_cg_array env ty c in
       let len = expression_of_const_generic env c in
       let dest = expression_of_place env dest in
       let repeat =
@@ -2006,14 +1972,16 @@ and expression_of_statement_kind (env : env) (ret_var : C.local_id) (s : C.state
             Krml.DeBruijn.(subst_t t 0 (subst_ct diff len 0 Builtin.array_repeat.typ))
             (ETApp (repeat, [ len ], [], [ t ])))
       in
-      Krml.Helpers.with_unit K.(EAssign (dest, with_type dest.typ (EApp (repeat, [ e ]))))
+      Krml.Helpers.with_unit K.(EAssign (dest, with_type dest.typ
+                               (expression_of_struct_Arr (with_type t_array (EApp (repeat, [e]))))))
+
   | Call
       {
         func =
           FnOpRegular
             {
               func = FunId (FBuiltin (Index { is_array = true; mutability = _; is_range = false }));
-              generics = { types = [ ty ]; _ };
+              generics = { types = [ ty ]; const_generics = [ cg ]; _ };
               _;
             };
         args = [ e1; e2 ];
@@ -2021,9 +1989,18 @@ and expression_of_statement_kind (env : env) (ret_var : C.local_id) (s : C.state
         _;
       } ->
       (* Special treatment because of the usage of maybe_addrof *)
+      (* Special treatment for e1[e2] of array which are translated into struct
+         e1[e2] is translated as fn ArrayIndexShared<T,N>(&[T;N], usize) -> &T
+
+         Since [T;N] is transalted into arr$T$N, we need to first dereference
+         the e1 to get the struct, and then take its field "data" to get the
+         array *)
       let e1 = expression_of_operand env e1 in
       let e2 = expression_of_operand env e2 in
       let t = typ_of_ty env ty in
+      let t_array = maybe_cg_array env ty cg in
+      let e1 = Krml.Helpers.(mk_deref (Krml.Helpers.assert_tbuf_or_tarray e1.K.typ) e1.K.node) in
+      let e1 = K.with_type t_array (K.EField (e1,"data")) in
       let dest = expression_of_place env dest in
       Krml.Helpers.with_unit
         K.(EAssign (dest, maybe_addrof env ty (with_type t (EBufRead (e1, e2)))))
@@ -2088,7 +2065,10 @@ and expression_of_statement_kind (env : env) (ret_var : C.local_id) (s : C.state
 
          This 100% does not work in case of a polymorphic function that is later monomorphized,
          meaning we really should be doing this transformation post-monomorphization. *)
-      let hd, output_t =
+
+      (** Array handling: commented special case for array *)
+      (*
+        let hd, output_t =
         match hd.node with
         | K.ETApp ({ node = EQualified lid; _ }, [], [], [ TArray (t, n) ])
           when lid = Builtin.box_new.name ->
@@ -2100,7 +2080,7 @@ and expression_of_statement_kind (env : env) (ret_var : C.local_id) (s : C.state
                   (ETApp (Builtin.(expr_of_builtin box_new_array), [ len ], [], [ t ]))),
               output_t )
         | _ -> hd, output_t
-      in
+      in *)
 
       let rhs =
         if args = [] then
@@ -2118,7 +2098,7 @@ and expression_of_statement_kind (env : env) (ret_var : C.local_id) (s : C.state
         in
         match fn_ptr.func, fn_ptr.generics.types @ extra_types with
         | ( FunId (FBuiltin (Index { is_array = false; mutability = _; is_range = false })),
-            [ TAdt { id = TBuiltin (TArray | TSlice); _ } ] ) ->
+            [ TAdt { id = TBuiltin (TSlice); _ } ] ) -> 
             (* Will decay. See comment above maybe_addrof *)
             rhs
         | ( FunId (FBuiltin (Index { is_array = false; mutability = _; is_range = false })),
@@ -2667,6 +2647,16 @@ let decls_of_declarations (env : env) (d : C.any_decl_id list) : K.decl list =
   L.log "Progress" "%s: %d/%d" env.crate_name !seen !total;
   Krml.KList.filter_some @@ List.map (decl_of_id env) d
 
+(*
+let impl_obligation (ob: decl_obligation) : K.decl =
+    match ob with ObliArray (lid, t_array) ->
+      L.log "AstOfLlbc" "append new decl of struct: %a" plid lid;
+      K.DType (lid, [], 1, 1, Flat [(Some "data",(t_array,true))])
+     
+let impl_obligations (obpairs : (decl_obligation * unit) list) : K.decl list =
+  List.map impl_obligation (List.map fst obpairs)
+  *)
+
 let file_of_crate (crate : Charon.LlbcAst.crate) : Krml.Ast.file =
   let {
     C.name;
@@ -2715,4 +2705,7 @@ let file_of_crate (crate : Charon.LlbcAst.crate) : Krml.Ast.file =
     }
   in
   let env = List.fold_left check_if_dst env declarations in
-  name, decls_of_declarations env declarations
+  let trans_decls = decls_of_declarations env declarations in
+  L.log "AstofLlbc" "Translated decls";
+  let extra_decls = [Builtin.decl_of_arr] in
+  name,  trans_decls @ extra_decls
diff --git a/lib/Builtin.ml b/lib/Builtin.ml
index 2e36770a..352a34f3 100644
--- a/lib/Builtin.ml
+++ b/lib/Builtin.ml
@@ -16,6 +16,20 @@ let range_from : K.lident = [ "core"; "ops"; "range" ], "RangeFrom"
 let mk_range_from (t : K.typ) : K.typ = K.TApp (range_from, [ t ])
 let option : K.lident = [ "core"; "option" ], "Option"
 let mk_option (t : K.typ) : K.typ = K.TApp (option, [ t ])
+
+(** special treatment for the array type: translating [T;C] as rust generic type
+    struct <const C:usize, T> { data : [T;C]; } *)
+
+let arr : K.lident = [ "Eurydice" ], "arr"
+let mk_arr (t : K.typ) (cg: K.cg) : K.typ = K.TCgApp (K.TApp (arr, [ t ]), cg)
+
+let decl_of_arr =
+  K.DType (arr , [], 1, 1, Flat [(Some "data", (K.TCgArray (TBound 0,0), true))])
+  (* []  : no flags
+     1  : we have one const generic C
+     1  : we have one type argument T *)
+
+
 let array_copy = [ "Eurydice" ], "array_copy"
 
 (* Things that could otherwise be emitted as an extern prototype, but for some
@@ -135,7 +149,7 @@ let get_128_op (kind, op) : K.expr = expr_of_builtin @@ Op128Map.find (kind, op)
 let array_to_slice =
   {
     name = [ "Eurydice" ], "array_to_slice";
-    typ = Krml.Helpers.fold_arrow [ TBuf (TBound 0, false) ] (mk_slice (TBound 0));
+    typ = Krml.Helpers.fold_arrow [ TBuf (mk_arr (TBound 0) (CgVar 0), false) ] (mk_slice (TBound 0));
     n_type_args = 1;
     cg_args = [ TInt SizeT ];
     arg_names = [ "a" ];
@@ -146,7 +160,7 @@ let array_to_subslice =
     name = [ "Eurydice" ], "array_to_subslice";
     typ =
       Krml.Helpers.fold_arrow
-        [ TBuf (TBound 2, false); mk_range (TInt SizeT) ]
+        [ TBuf (mk_arr (TBound 2) (CgVar 0), false); mk_range (TInt SizeT) ]
         (mk_slice (TBound 2));
     n_type_args = 3;
     cg_args = [ TInt SizeT ];
@@ -158,7 +172,7 @@ let array_to_subslice_to =
     name = [ "Eurydice" ], "array_to_subslice_to";
     typ =
       Krml.Helpers.fold_arrow
-        [ TBuf (TBound 2, false); mk_range_to (TInt SizeT) ]
+        [ TBuf (mk_arr (TBound 2) (CgVar 0), false); mk_range_to (TInt SizeT) ]
         (mk_slice (TBound 2));
     n_type_args = 3;
     cg_args = [ TInt SizeT ];
@@ -170,7 +184,7 @@ let array_to_subslice_from =
     name = [ "Eurydice" ], "array_to_subslice_from";
     typ =
       Krml.Helpers.fold_arrow
-        [ TBuf (TBound 2, false); mk_range_from (TInt SizeT) ]
+        [ TBuf (mk_arr (TBound 2) (CgVar 0), false); mk_range_from (TInt SizeT) ]
         (mk_slice (TBound 2));
     n_type_args = 3;
     cg_args = [ TInt SizeT ];
@@ -217,9 +231,7 @@ let array_into_iter =
 let array_eq =
   {
     name = [ "Eurydice" ], "array_eq";
-    (* This is NOT `Krml.Helpers.fold_arrow [ TCgArray (TBound 0, 0); TCgArray (TBound 0, 0) ]
-       TBool` because we get array pointers that decay. *)
-    typ = Krml.Helpers.fold_arrow [ TBuf (TBound 0, false); TBuf (TBound 0, false) ] TBool;
+    typ = Krml.Helpers.fold_arrow [ TBuf (mk_arr (TBound 0) (CgVar 0), false); TBuf (mk_arr (TBound 0) (CgVar 0), false) ] TBool;
     n_type_args = 1;
     cg_args = [ TInt SizeT ];
     arg_names = [ "arr"; "arr2" ];
@@ -228,8 +240,7 @@ let array_eq =
 let array_eq_slice =
   {
     name = [ "Eurydice" ], "array_eq_slice";
-    typ =
-      Krml.Helpers.fold_arrow [ TBuf (TBound 0, false); TBuf (mk_slice (TBound 0), false) ] TBool;
+    typ = Krml.Helpers.fold_arrow [ TBuf (mk_arr (TBound 0) (CgVar 0), false); TBuf (mk_slice (TBound 0), false) ] TBool;
     n_type_args = 1;
     cg_args = [ TInt SizeT ];
     arg_names = [ "arr"; "slice" ];
@@ -367,13 +378,13 @@ let box_new =
     arg_names = [ "v" ];
   }
 
-let box_new_array =
+let empty_array =
   {
-    name = [ "Eurydice" ], "box_new_array";
-    typ = Krml.Helpers.fold_arrow [ TCgArray (TBound 0, 0) ] (TBuf (TBound 0, false));
+    name = [ "Eurydice" ], "empty_array";
+    typ = Krml.Helpers.fold_arrow [ TBound 0 ] (mk_arr (TBound 0) (CgConst (SizeT, "0")));
     n_type_args = 1;
-    cg_args = [ TInt SizeT ];
-    arg_names = [ "v" ];
+    cg_args = [];
+    arg_names = [ "x" ];
   }
 
 let replace =
@@ -433,16 +444,6 @@ let slice_of_dst =
     arg_names = [ "ptr"; "len" ];
   }
 
-(* Gotta use a helper because the definition of Eurydice_slice is opaque (historical mistake?). *)
-let slice_of_boxed_array =
-  {
-    name = [ "Eurydice" ], "slice_of_boxed_array";
-    typ = Krml.Helpers.fold_arrow [ TBuf (TBound 0, false); TInt SizeT ] (mk_slice (TBound 0));
-    n_type_args = 1;
-    cg_args = [];
-    arg_names = [ "ptr"; "len" ];
-  }
-
 (* Take the type of the ptr field *)
 let dst_new ~ptr ~len t =
   let open K in
@@ -754,10 +755,9 @@ let builtin_funcs =
     range_iterator_step_by;
     range_step_by_iterator_next;
     box_new;
-    box_new_array;
+    empty_array;
     replace;
     slice_of_dst;
-    slice_of_boxed_array;
     bitand_pv_u8;
     shr_pv_u8;
     min_u32;
diff --git a/lib/Cleanup2.ml b/lib/Cleanup2.ml
index 1cc5c5ac..44bb5dd1 100644
--- a/lib/Cleanup2.ml
+++ b/lib/Cleanup2.ml
@@ -209,7 +209,7 @@ let remove_array_repeats =
              let the subsequent `hoist` phase lift this into a let-binding, and code-gen will optimize this into
              { 0 }. If we can't do something smart, we let-bind, and fall back onto the general case. *)
           begin
-            try (self#expand_repeat false (with_type (snd env) (EApp (e, es)))).node
+            try (self#expand_repeat (fst env) (with_type (snd env) (EApp (e, es)))).node
             with Not_found ->
               (self#visit_expr env
                  (with_type (snd env)
@@ -226,6 +226,11 @@ let remove_array_repeats =
       | EConstant (_, s) -> int_of_string s
       | _ -> failwith "impossible"
 
+    method private is_arr_typ t =
+      match t with
+      | TQualified ( [ s1 ], s2) -> s1 = "Eurydice" && String.sub s2 0 3 = "arr"
+      | _ -> false
+
     (* This function recursively expands nested repeat expressions as initializer lists
        (EBufCreateL) as long as the innermost initial value is a zero, otherwise, it throws
        Not_found. For instance:
@@ -233,11 +238,12 @@ let remove_array_repeats =
        - [[1; 2]; 2] --> error -- better code quality with a BufCreate expression which will give
          rise to a for-loop initializer
 
-       We override this behavior when we're already underneath an EBufCreateL -- here, we've already
+       We override this behavior when we're already underneath a visit_DGlobal -- here, we've already
        committed to an initializer list (and Charon will suitably "fold" repeat expressions
        automatically for us), so we might as well expand.
+       
     *)
-    method private expand_repeat under_bufcreate e =
+    method private expand_repeat under_global e =
       match e.node with
       | EApp
           ( { node = ETApp ({ node = EQualified lid; _ }, [ len ], _, [ _ ]); _ },
@@ -245,47 +251,33 @@ let remove_array_repeats =
         when lid = Builtin.array_repeat.name ->
           (* [0; n] -> ok *)
           with_type e.typ @@ EBufCreateL (Stack, List.init (self#assert_length len) (fun _ -> init))
+      | EApp
+          ( { node = ETApp ({ node = EQualified lid; _ }, [ len ], _, [ _ ]); _ },
+            [ ({ node = EConstant _; _ } as init) ] )
+        when lid = Builtin.array_repeat.name && under_global ->
+          (* [c; n] -> get translated when we are under DGlobal *)
+          with_type e.typ @@ EBufCreate (Stack, init, Krml.Helpers.mk_sizet (self#assert_length len))
       | EApp ({ node = ETApp ({ node = EQualified lid; _ }, [ len ], _, [ _ ]); _ }, [ init ])
         when lid = Builtin.array_repeat.name ->
           (* [e; n] -> ok if e ok -- n is a constant here Rust has no VLAs *)
-          let init = self#expand_repeat under_bufcreate init in
+          let init = self#expand_repeat under_global init in
           with_type e.typ @@ EBufCreateL (Stack, List.init (self#assert_length len) (fun _ -> init))
+      | EFlat [ (lido, e1) ] when lido = Some "data" && self#is_arr_typ e.typ ->
+         (* { .data = e } -> ok if e ok *)
+         let e1 = self#expand_repeat under_global e1 in
+         with_type e.typ (EFlat [lido, e1])
+      | EBufCreateL (l, es) when under_global ->
+         (* { e1, e2, ... en } -> get recursively expanded when are under DGlobal *)
+         with_type e.typ @@ EBufCreateL (l, List.map (self#expand_repeat true) es)
       | _ ->
-          if under_bufcreate then
+          if under_global then
             e
           else
             raise Not_found
 
-    method! visit_DGlobal env flags name n t e1 =
-      match e1.node with
-      | EBufCreateL (l, es) ->
-          DGlobal
-            ( flags,
-              name,
-              n,
-              t,
-              with_type e1.typ (EBufCreateL (l, List.map (self#expand_repeat true) es)) )
-      | EApp ({ node = ETApp ({ node = EQualified lid; _ }, [ len ], _, [ _ ]); _ }, [ init ])
-        when lid = Builtin.array_repeat.name -> begin
-          try
-            (* Case 1. *)
-            DGlobal (flags, name, n, t, (self#expand_repeat false) e1)
-          with Not_found -> (
-            match init.node with
-            | EConstant _ ->
-                (* Case 2. *)
-                DGlobal
-                  ( flags,
-                    name,
-                    n,
-                    t,
-                    with_type e1.typ
-                      (EBufCreate (Stack, init, Krml.Helpers.mk_sizet (self#assert_length len))) )
-            | _ -> super#visit_DGlobal env flags name n t e1)
-        end
-      | _ -> super#visit_DGlobal env flags name n t e1
+    method! visit_DGlobal _env flags name n t e1 = super#visit_DGlobal true flags name n t e1
 
-    method! visit_ELet (((), _) as env) b e1 e2 =
+    method! visit_ELet ((under_global, _) as env) b e1 e2 =
       match e1.node with
       (* Nothing special here for EBufCreateL otherwise it breaks the invariant expected by
          remove_implicit_array_copies *)
@@ -293,7 +285,7 @@ let remove_array_repeats =
         when lid = Builtin.array_repeat.name -> begin
           try
             (* Case 1 (only zeroes). *)
-            let r = ELet (b, (self#expand_repeat false) e1, self#visit_expr env e2) in
+            let r = ELet (b, (self#expand_repeat under_global) e1, self#visit_expr env e2) in
             r
           with Not_found -> (
             match init.node with
@@ -362,40 +354,31 @@ let remove_array_from_fn files =
               [ len ],
               [ call_mut; _call_once ],
               [ t_elements; _t_captured_state ] ) ->
-            (* Same as below, but catching the case where the type of elements is an
-               array and has undergone outparam optimization (i.e. the closure,
-               instead of having type size_t -> t_element, has type size_t -> t_element ->
-               unit *)
             L.log "Cleanup2" "%a %a" ptyp t_elements ptyp t_elements;
-            (* First argument = closure, second argument = destination. Note that
-               the closure may itself be an application of the closure to the state
-               (but not always... is this unit argument elimination kicking in? not
-               sure). *)
-            let state, dst =
-              match es with
-              | [ x; y ] -> x, y
+            (* By translating array into struct, we return a struct of array for [from_fn] here *)
+            let state = Krml.KList.one es in
+            let t_struct, _ = Krml.Helpers.flatten_arrow e.typ in
+            let t_element, _ = Krml.Helpers.flatten_arrow call_mut.typ in
+            let t_array =
+              match len.node with
+              | EConstant c -> TArray (t_element, c)
               | _ -> assert false
             in
-            let lift1 = Krml.DeBruijn.lift 1 in
-            let t_dst = H.assert_tbuf_or_tarray dst.typ in
-            EFor
-              ( Krml.Helpers.fresh_binder ~mut:true "i" H.usize,
-                H.zero_usize (* i: size_t = 0 *),
-                H.mk_lt_usize (Krml.DeBruijn.lift 1 len) (* i < len *),
-                H.mk_incr_usize (* i++ *),
-                let i = with_type H.usize (EBound 0) in
-                Krml.Helpers.with_unit
-                  (if H.is_array t_dst then
-                     EApp
-                       ( call_mut,
-                         [
-                           with_type (TBuf (state.typ, false)) (EAddrOf (lift1 state));
-                           with_type (TInt SizeT) (EBound 0);
-                           with_type t_dst (EBufRead (lift1 dst, i));
-                         ] )
-                   else
-                     EBufWrite
-                       ( Krml.DeBruijn.lift 1 dst,
+            let x, dst_struct = H.mk_binding ~mut:true "arr_struct" t_struct in
+            let dst = with_type (t_array) (EField (dst_struct, "data")) in
+            let bindx = (x, with_type t_struct EAny) in
+            let t_dst = H.assert_tbuf_or_tarray t_array in
+            let for_assign = 
+              let lift1 = Krml.DeBruijn.lift 1 in
+              with_type TUnit (EFor
+                ( Krml.Helpers.fresh_binder ~mut:true "i" H.usize,
+                  H.zero_usize (* i: size_t = 0 *),
+                  H.mk_lt_usize (Krml.DeBruijn.lift 1 len) (* i < len *),
+                  H.mk_incr_usize (* i++ *),
+                  let i = with_type H.usize (EBound 0) in
+                  Krml.Helpers.with_unit
+                     (EBufWrite
+                       ( lift1 dst,
                          i,
                          with_type t_dst
                            (EApp
@@ -403,7 +386,8 @@ let remove_array_from_fn files =
                                 [
                                   with_type (TBuf (state.typ, false)) (EAddrOf (lift1 state));
                                   with_type (TInt SizeT) (EBound 0);
-                                ] )) )) )
+                ] )) )) ))
+             in (H.nest [bindx] t_struct (with_type t_struct (ESequence [for_assign; dst_struct]))).node
         | ETApp
             ( { node = EQualified ("core" :: "array" :: _, "map"); _ },
               [ len ],
@@ -418,14 +402,26 @@ let remove_array_from_fn files =
               | _ ->
                   failwith "TODO: unknown map closure shape; is it an array outparam? (see above)"
             in
-            let e_src, e_state, e_dst =
+            let e_src, e_state =
               match es with
-              | [ e_src; e_state; e_dst ] -> e_src, e_state, e_dst
+              | [ e_src; e_state ] -> e_src, e_state
               | _ -> failwith "unknown shape of arguments to array map"
             in
+            let len_c =
+              match len.node with
+              | EConstant c -> c
+              | _ -> failwith "unable to get the const length for array map"
+            in
             let lift1 = Krml.DeBruijn.lift 1 in
             let e_state = with_type (TBuf (e_state.typ, false)) (EAddrOf (lift1 e_state)) in
-            EFor
+            let e_src = with_type (TArray (t_src, len_c)) (EField (e_src, "data")) in
+            let t_dst_str, _ = Krml.Helpers.flatten_arrow e.typ in
+            let t_dst_arr = TArray (t_dst, len_c) in
+            let x, dst_struct = H.mk_binding ~mut:true "arr_mapped_str" t_dst_str in
+            let e_dst = with_type (t_dst_arr) (EField (dst_struct, "data")) in
+            let bindx = (x, with_type t_dst_str EAny) in
+            let for_assign = 
+              with_type TUnit (EFor
               ( Krml.Helpers.fresh_binder ~mut:true "i" H.usize,
                 H.zero_usize (* i = 0 *),
                 H.mk_lt_usize (Krml.DeBruijn.lift 1 len) (* i < len *),
@@ -435,7 +431,8 @@ let remove_array_from_fn files =
                 Krml.Helpers.with_unit
                   (EBufWrite
                      (lift1 e_dst, i, with_type t_dst (EApp (call_mut, [ lift1 e_state; e_src_i ]))))
-              )
+              ))
+            in (H.nest [bindx] t_dst_str (with_type t_dst_str (ESequence [for_assign; dst_struct]))).node 
         | _ -> super#visit_EApp env e es
     end
   end
diff --git a/lib/Cleanup3.ml b/lib/Cleanup3.ml
index c8bf22f4..78ca946c 100644
--- a/lib/Cleanup3.ml
+++ b/lib/Cleanup3.ml
@@ -159,6 +159,22 @@ let add_extra_type_to_slice_index =
       | _ -> super#visit_EApp env e es
   end
 
+(*This identifies the decls which should be generated after monomorphism, but is already defined
+ in eurydice_glue.h for implementing the builtin functions. Currently only for arr<T;N> *)
+let is_builtin_lid lid = match lid with
+  | ([ "Eurydice" ], "arr_c4") (* arr {data:[u8;8]}*)
+  | ([ "Eurydice" ], "arr_e9") (* arr {data:[u8;4]}*)
+  | ([ "Eurydice" ], "arr_8b") (* arr {data:[u8,2]}*)
+     -> true
+  | _ -> false
+
+let remove_builtin_decls files =
+  let checker = function
+    | DType (lid, _, _, _, _) when is_builtin_lid lid -> None
+    | decl -> Some decl
+  in
+  List.map (fun (name, decls) -> name, List.filter_map checker decls) files
+
 let also_skip_prefix_for_external_types (scope_env, _) =
   let open Krml in
   object (_self)
diff --git a/lib/PreCleanup.ml b/lib/PreCleanup.ml
index aad43704..0413c1b5 100644
--- a/lib/PreCleanup.ml
+++ b/lib/PreCleanup.ml
@@ -46,31 +46,32 @@ let expand_array_copies files =
 let remove_array_eq =
   object
     inherit Krml.DeBruijn.map_counting_cg as super
-
-    method! visit_expr (((n_cgs, n_binders) as env), _) e =
-      match e with
-      | [%cremepat {| core::array::equality::?impl::eq[#?n](#?..)<?t,?u>(?a1, ?a2) |}] ->
-          let rec is_flat = function
-            | TArray (t, _) -> is_flat t
-            | TInt _ | TBool | TUnit -> true
-            | _ -> false
-          in
-          assert (t = u);
-          if is_flat t then
-            let diff = n_binders - n_cgs in
-            match impl with
-            | "{core::cmp::PartialEq<@Array<U, N>> for @Array<T, N>}" ->
-                with_type TBool
-                  (EApp (Builtin.(expr_of_builtin_t ~cgs:(diff, [ n ]) array_eq [ t ]), [ a1; a2 ]))
-            | "{core::cmp::PartialEq<&0 (@Slice<U>)> for @Array<T, N>}" ->
-                with_type TBool
-                  (EApp
-                     ( Builtin.(expr_of_builtin_t ~cgs:(diff, [ n ]) array_eq_slice [ t ]),
-                       [ a1; a2 ] ))
-            | _ -> failwith ("unknown array eq impl: " ^ impl)
-          else
-            failwith "TODO: non-byteeq array comparison"
-      | _ -> super#visit_expr (env, e.typ) e
+    
+  method! visit_expr ((n_cgs, n_binders) as env, _) e =
+    match e with
+    | [%cremepat {| core::array::equality::?impl::eq[#?n](#?..)<?t,?u>(?a1, ?a2) |}] ->
+        let rec is_flat = function
+          | TCgApp (TApp (lid, [ t ]), _) -> lid = Builtin.arr && is_flat t
+          | TInt _ | TBool | TUnit -> true
+          | _ -> false
+        in
+        assert (t = u);
+        if is_flat t then
+          let diff = n_binders - n_cgs in
+          match impl with
+          | "{core::cmp::PartialEq<@Array<U, N>> for @Array<T, N>}" ->
+              with_type TBool (EApp (
+                Builtin.(expr_of_builtin_t ~cgs:(diff, [n]) array_eq [ t ]),
+                [ a1; a2 ]))
+          | "{core::cmp::PartialEq<&0 (@Slice<U>)> for @Array<T, N>}" ->
+              with_type TBool (EApp (
+                Builtin.(expr_of_builtin_t ~cgs:(diff, [n]) array_eq_slice [ t ]),
+                [ a1; a2 ]))
+          | _ ->
+              failwith ("unknown array eq impl: " ^ impl)
+        else
+          failwith "TODO: non-byteeq array comparison"
+    | _ -> super#visit_expr (env, e.typ) e
 
     method! visit_DFunction _ cc flags n_cgs n t lid bs e =
       super#visit_DFunction (n_cgs, 0) cc flags n_cgs n t lid bs e
diff --git a/out/test-array/array.c b/out/test-array/array.c
index 83519e59..17d527f8 100644
--- a/out/test-array/array.c
+++ b/out/test-array/array.c
@@ -9,20 +9,13 @@
 
 array_Foo array_mk_foo(void)
 {
-  uint32_t x[2U] = { 0U };
-  uint32_t y[2U];
+  Eurydice_arr_b2 x = { .data = { 0U } };
+  Eurydice_arr_b2 y;
+  uint32_t repeat_expression[2U];
   for (uint32_t _i = 0U; _i < (size_t)2U; ++_i)
-    y[_i] = 1U;
-  /* Passing arrays by value in Rust generates a copy in C */
-  uint32_t copy_of_x[2U];
-  memcpy(copy_of_x, x, (size_t)2U * sizeof (uint32_t));
-  /* Passing arrays by value in Rust generates a copy in C */
-  uint32_t copy_of_y[2U];
-  memcpy(copy_of_y, y, (size_t)2U * sizeof (uint32_t));
-  array_Foo lit;
-  memcpy(lit.x, copy_of_x, (size_t)2U * sizeof (uint32_t));
-  memcpy(lit.y, copy_of_y, (size_t)2U * sizeof (uint32_t));
-  return lit;
+    repeat_expression[_i] = 1U;
+  memcpy(y.data, repeat_expression, (size_t)2U * sizeof (uint32_t));
+  return (KRML_CLITERAL(array_Foo){ .x = x, .y = y });
 }
 
 array_Foo array_mk_foo2(void)
@@ -30,17 +23,17 @@ array_Foo array_mk_foo2(void)
   return array_mk_foo();
 }
 
-void array_mut_array(uint32_t x[2U])
+void array_mut_array(Eurydice_arr_b2 x)
 {
-  x[0U] = 1U;
+  x.data[0U] = 1U;
 }
 
 void array_mut_foo(array_Foo f)
 {
-  f.x[0U] = 1U;
-  uint32_t copy[2U];
-  memcpy(copy, f.y, (size_t)2U * sizeof (uint32_t));
-  copy[0U] = 0U;
+  f.x.data[0U] = 1U;
+  Eurydice_arr_b2 copy = f.y;
+  copy.data[0U] = 0U;
+  EURYDICE_ASSERT(copy.data[0U] != 1U, "panic!");
 }
 
 /**
@@ -77,15 +70,17 @@ A monomorphic instance of array.mk_incr
 with const generics
 - K= 10
 */
-void array_mk_incr_95(uint32_t ret[10U])
+Eurydice_arr_79 array_mk_incr_95(void)
 {
+  Eurydice_arr_79 arr_struct;
   KRML_MAYBE_FOR10(i,
     (size_t)0U,
     (size_t)10U,
     (size_t)1U,
     /* original Rust expression is not an lvalue in C */
     void *lvalue = (void *)0U;
-    ret[i] = array_mk_incr_call_mut_e2_95(&lvalue, i););
+    arr_struct.data[i] = array_mk_incr_call_mut_e2_95(&lvalue, i););
+  return arr_struct;
 }
 
 /**
@@ -120,18 +115,18 @@ A monomorphic instance of array.mk_incr2
 with const generics
 - K= 10
 */
-void array_mk_incr2_95(uint32_t ret[10U])
+Eurydice_arr_79 array_mk_incr2_95(void)
 {
   uint32_t j = 1U;
-  uint32_t ret0[10U];
+  Eurydice_arr_79 arr_struct;
   KRML_MAYBE_FOR10(i,
     (size_t)0U,
     (size_t)10U,
     (size_t)1U,
     /* original Rust expression is not an lvalue in C */
     uint32_t *lvalue = &j;
-    ret0[i] = array_mk_incr2_call_mut_eb_95(&lvalue, i););
-  memcpy(ret, ret0, (size_t)10U * sizeof (uint32_t));
+    arr_struct.data[i] = array_mk_incr2_call_mut_eb_95(&lvalue, i););
+  return arr_struct;
 }
 
 /**
@@ -168,18 +163,15 @@ A monomorphic instance of array.plus_one
 with const generics
 - K= 1
 */
-void array_plus_one_74(uint32_t x[1U], uint16_t ret[1U])
+Eurydice_arr_2e array_plus_one_74(Eurydice_arr_a5 x)
 {
-  /* Passing arrays by value in Rust generates a copy in C */
-  uint32_t copy_of_x[1U];
-  memcpy(copy_of_x, x, (size_t)1U * sizeof (uint32_t));
-  uint16_t ret0[1U];
+  Eurydice_arr_2e arr_mapped_str;
   {
     /* original Rust expression is not an lvalue in C */
     void *lvalue = (void *)0U;
-    ret0[0U] = array_plus_one_call_mut_8d_74(&lvalue, copy_of_x[0U]);
+    arr_mapped_str.data[0U] = array_plus_one_call_mut_8d_74(&lvalue, x.data[0U]);
   }
-  memcpy(ret, ret0, (size_t)1U * sizeof (uint16_t));
+  return arr_mapped_str;
 }
 
 /**
@@ -217,18 +209,18 @@ A monomorphic instance of array.nested_from_fn.call_mut_af
 with const generics
 - K= 4
 */
-void array_nested_from_fn_call_mut_af_ac(void **_, size_t tupled_args, size_t ret[4U])
+Eurydice_arr_33 array_nested_from_fn_call_mut_af_ac(void **_, size_t tupled_args)
 {
   size_t j = tupled_args;
-  size_t ret0[4U];
+  Eurydice_arr_33 arr_struct;
   KRML_MAYBE_FOR4(i,
     (size_t)0U,
     (size_t)4U,
     (size_t)1U,
     /* original Rust expression is not an lvalue in C */
     size_t *lvalue = &j;
-    ret0[i] = array_nested_from_fn_closure_call_mut_74_ac(&lvalue, i););
-  memcpy(ret, ret0, (size_t)4U * sizeof (size_t));
+    arr_struct.data[i] = array_nested_from_fn_closure_call_mut_74_ac(&lvalue, i););
+  return arr_struct;
 }
 
 /**
@@ -239,11 +231,11 @@ A monomorphic instance of array.nested_from_fn.call_once_f6
 with const generics
 - K= 4
 */
-void array_nested_from_fn_call_once_f6_ac(size_t _, size_t ret[4U])
+Eurydice_arr_33 array_nested_from_fn_call_once_f6_ac(size_t _)
 {
   /* original Rust expression is not an lvalue in C */
   void *lvalue = (void *)0U;
-  array_nested_from_fn_call_mut_af_ac(&lvalue, _, ret);
+  return array_nested_from_fn_call_mut_af_ac(&lvalue, _);
 }
 
 /**
@@ -251,15 +243,27 @@ A monomorphic instance of array.nested_from_fn
 with const generics
 - K= 4
 */
-void array_nested_from_fn_ac(size_t ret[4U][4U])
+Eurydice_arr_11 array_nested_from_fn_ac(void)
 {
+  Eurydice_arr_11 arr_struct;
   KRML_MAYBE_FOR4(i,
     (size_t)0U,
     (size_t)4U,
     (size_t)1U,
     /* original Rust expression is not an lvalue in C */
     void *lvalue = (void *)0U;
-    array_nested_from_fn_call_mut_af_ac(&lvalue, i, ret[i]););
+    arr_struct.data[i] = array_nested_from_fn_call_mut_af_ac(&lvalue, i););
+  return arr_struct;
+}
+
+/**
+A monomorphic instance of array.const_eq
+with const generics
+- K= 2
+*/
+bool array_const_eq_fd(Eurydice_arr_b2 x, Eurydice_arr_b2 y)
+{
+  return Eurydice_array_eq((size_t)2U, &x, &y, uint32_t);
 }
 
 typedef struct _uint32_t__x2_s
@@ -283,55 +287,62 @@ typedef struct _size_t__x2_s
 }
 _size_t__x2;
 
+typedef struct _bool__x2_s
+{
+  bool *fst;
+  bool *snd;
+}
+_bool__x2;
+
 void array_main(void)
 {
   /* XXX1 */
   array_Foo uu____0 = array_mk_foo2();
-  uint32_t x[2U];
-  memcpy(x, uu____0.x, (size_t)2U * sizeof (uint32_t));
-  /* XXX2 */
-  uint32_t y[2U];
-  memcpy(y, uu____0.y, (size_t)2U * sizeof (uint32_t));
+  Eurydice_arr_b2 x = uu____0.x;
+  Eurydice_arr_b2 y = uu____0.y;
   uint32_t unsigned0 = 0U;
-  uint32_t uu____1[2U];
-  memcpy(uu____1, x, (size_t)2U * sizeof (uint32_t));
-  array_mut_array(uu____1);
-  /* Passing arrays by value in Rust generates a copy in C */
-  uint32_t copy_of_x[2U];
-  memcpy(copy_of_x, x, (size_t)2U * sizeof (uint32_t));
-  /* Passing arrays by value in Rust generates a copy in C */
-  uint32_t copy_of_y[2U];
-  memcpy(copy_of_y, y, (size_t)2U * sizeof (uint32_t));
-  array_Foo lit;
-  memcpy(lit.x, copy_of_x, (size_t)2U * sizeof (uint32_t));
-  memcpy(lit.y, copy_of_y, (size_t)2U * sizeof (uint32_t));
-  array_mut_foo(lit);
-  _uint32_t__x2 uu____4 = { .fst = x, .snd = &unsigned0 };
-  EURYDICE_ASSERT(uu____4.fst[0U] == uu____4.snd[0U], "panic!");
-  uint32_t a[10U];
-  array_mk_incr_95(a);
+  array_mut_array(x);
+  /* XXX2 */
+  array_mut_foo((KRML_CLITERAL(array_Foo){ .x = x, .y = y }));
+  /* XXX3
+    XXX4 */
+  _uint32_t__x2 uu____1 = { .fst = x.data, .snd = &unsigned0 };
+  EURYDICE_ASSERT(uu____1.fst[0U] == uu____1.snd[0U], "panic!");
+  Eurydice_arr_79 a = array_mk_incr_95();
   /* original Rust expression is not an lvalue in C */
   uint32_t lvalue0 = 9U;
-  _uint32_t__x2 uu____5 = { .fst = &a[9U], .snd = &lvalue0 };
-  EURYDICE_ASSERT(uu____5.fst[0U] == uu____5.snd[0U], "panic!");
-  uint32_t a0[10U];
-  array_mk_incr2_95(a0);
+  _uint32_t__x2 uu____2 = { .fst = &a.data[9U], .snd = &lvalue0 };
+  EURYDICE_ASSERT(uu____2.fst[0U] == uu____2.snd[0U], "panic!");
+  Eurydice_arr_79 a0 = array_mk_incr2_95();
   uint32_t expected = 10U;
-  _uint32_t__x2 uu____6 = { .fst = &a0[9U], .snd = &expected };
-  EURYDICE_ASSERT(uu____6.fst[0U] == uu____6.snd[0U], "panic!");
-  uint16_t a1[1U];
-  uint32_t buf[1U] = { 0U };
-  array_plus_one_74(buf, a1);
+  _uint32_t__x2 uu____3 = { .fst = &a0.data[9U], .snd = &expected };
+  EURYDICE_ASSERT(uu____3.fst[0U] == uu____3.snd[0U], "panic!");
+  Eurydice_arr_2e a1 = array_plus_one_74((KRML_CLITERAL(Eurydice_arr_a5){ .data = { 0U } }));
   /* original Rust expression is not an lvalue in C */
   uint16_t lvalue1 = 1U;
-  _uint16_t__x2 uu____7 = { .fst = a1, .snd = &lvalue1 };
-  EURYDICE_ASSERT(uu____7.fst[0U] == uu____7.snd[0U], "panic!");
+  _uint16_t__x2 uu____4 = { .fst = a1.data, .snd = &lvalue1 };
+  EURYDICE_ASSERT(uu____4.fst[0U] == uu____4.snd[0U], "panic!");
   /* XXX5 */
-  size_t a2[4U][4U];
-  array_nested_from_fn_ac(a2);
+  Eurydice_arr_11 a2 = array_nested_from_fn_ac();
   /* original Rust expression is not an lvalue in C */
-  size_t lvalue = (size_t)6U;
-  _size_t__x2 uu____8 = { .fst = &a2[3U][3U], .snd = &lvalue };
-  EURYDICE_ASSERT(uu____8.fst[0U] == uu____8.snd[0U], "panic!");
+  size_t lvalue2 = (size_t)6U;
+  _size_t__x2 uu____5 = { .fst = &a2.data[3U].data[3U], .snd = &lvalue2 };
+  EURYDICE_ASSERT(uu____5.fst[0U] == uu____5.snd[0U], "panic!");
+  /* XXX6 */
+  Eurydice_arr_b2 x0;
+  uint32_t repeat_expression0[2U];
+  for (uint32_t _i = 0U; _i < (size_t)2U; ++_i)
+    repeat_expression0[_i] = 2U;
+  memcpy(x0.data, repeat_expression0, (size_t)2U * sizeof (uint32_t));
+  Eurydice_arr_b2 y0;
+  uint32_t repeat_expression[2U];
+  for (uint32_t _i = 0U; _i < (size_t)2U; ++_i)
+    repeat_expression[_i] = 2U;
+  memcpy(y0.data, repeat_expression, (size_t)2U * sizeof (uint32_t));
+  bool b = array_const_eq_fd(x0, y0);
+  /* original Rust expression is not an lvalue in C */
+  bool lvalue = true;
+  _bool__x2 uu____6 = { .fst = &b, .snd = &lvalue };
+  EURYDICE_ASSERT(uu____6.fst[0U] == uu____6.snd[0U], "panic!");
 }
 
diff --git a/out/test-array/array.h b/out/test-array/array.h
index bc000a76..7ce39280 100644
--- a/out/test-array/array.h
+++ b/out/test-array/array.h
@@ -15,13 +15,23 @@
 extern "C" {
 #endif
 
+/**
+A monomorphic instance of Eurydice.arr
+with types uint32_t
+with const generics
+- $2size_t
+*/
+typedef struct Eurydice_arr_b2_s { uint32_t data[2U]; } Eurydice_arr_b2;
+
 typedef struct array_Foo_s
 {
-  uint32_t x[2U];
-  uint32_t y[2U];
+  Eurydice_arr_b2 x;
+  Eurydice_arr_b2 y;
 }
 array_Foo;
 
+extern bool core_cmp_impls__core__cmp__PartialEq_u32__for_u32__eq(uint32_t *x0, uint32_t *x1);
+
 #define core_panicking_AssertKind_Eq 0
 #define core_panicking_AssertKind_Ne 1
 #define core_panicking_AssertKind_Match 2
@@ -32,7 +42,7 @@ array_Foo array_mk_foo(void);
 
 array_Foo array_mk_foo2(void);
 
-void array_mut_array(uint32_t x[2U]);
+void array_mut_array(Eurydice_arr_b2 x);
 
 void array_mut_foo(array_Foo f);
 
@@ -56,12 +66,20 @@ with const generics
 */
 uint32_t array_mk_incr_call_once_b7_95(size_t _);
 
+/**
+A monomorphic instance of Eurydice.arr
+with types uint32_t
+with const generics
+- $10size_t
+*/
+typedef struct Eurydice_arr_79_s { uint32_t data[10U]; } Eurydice_arr_79;
+
 /**
 A monomorphic instance of array.mk_incr
 with const generics
 - K= 10
 */
-void array_mk_incr_95(uint32_t ret[10U]);
+Eurydice_arr_79 array_mk_incr_95(void);
 
 /**
 A monomorphic instance of array.mk_incr2.closure
@@ -95,7 +113,7 @@ A monomorphic instance of array.mk_incr2
 with const generics
 - K= 10
 */
-void array_mk_incr2_95(uint32_t ret[10U]);
+Eurydice_arr_79 array_mk_incr2_95(void);
 
 /**
 This function found in impl {core::ops::function::FnMut<(u32), u16> for array::plus_one::closure<K>}
@@ -117,12 +135,28 @@ with const generics
 */
 uint16_t array_plus_one_call_once_36_74(uint32_t _);
 
+/**
+A monomorphic instance of Eurydice.arr
+with types uint16_t
+with const generics
+- $1size_t
+*/
+typedef struct Eurydice_arr_2e_s { uint16_t data[1U]; } Eurydice_arr_2e;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types uint32_t
+with const generics
+- $1size_t
+*/
+typedef struct Eurydice_arr_a5_s { uint32_t data[1U]; } Eurydice_arr_a5;
+
 /**
 A monomorphic instance of array.plus_one
 with const generics
 - K= 1
 */
-void array_plus_one_74(uint32_t x[1U], uint16_t ret[1U]);
+Eurydice_arr_2e array_plus_one_74(Eurydice_arr_a5 x);
 
 /**
 A monomorphic instance of array.nested_from_fn.closure.closure
@@ -151,6 +185,14 @@ with const generics
 */
 size_t array_nested_from_fn_closure_call_once_4d_ac(size_t *_, size_t _0);
 
+/**
+A monomorphic instance of Eurydice.arr
+with types size_t
+with const generics
+- $4size_t
+*/
+typedef struct Eurydice_arr_33_s { size_t data[4U]; } Eurydice_arr_33;
+
 /**
 This function found in impl {core::ops::function::FnMut<(usize), @Array<usize, K>> for array::nested_from_fn::closure<K>}
 */
@@ -159,7 +201,7 @@ A monomorphic instance of array.nested_from_fn.call_mut_af
 with const generics
 - K= 4
 */
-void array_nested_from_fn_call_mut_af_ac(void **_, size_t tupled_args, size_t ret[4U]);
+Eurydice_arr_33 array_nested_from_fn_call_mut_af_ac(void **_, size_t tupled_args);
 
 /**
 This function found in impl {core::ops::function::FnOnce<(usize), @Array<usize, K>> for array::nested_from_fn::closure<K>}
@@ -169,14 +211,29 @@ A monomorphic instance of array.nested_from_fn.call_once_f6
 with const generics
 - K= 4
 */
-void array_nested_from_fn_call_once_f6_ac(size_t _, size_t ret[4U]);
+Eurydice_arr_33 array_nested_from_fn_call_once_f6_ac(size_t _);
+
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr size_t[[$4size_t]]
+with const generics
+- $4size_t
+*/
+typedef struct Eurydice_arr_11_s { Eurydice_arr_33 data[4U]; } Eurydice_arr_11;
 
 /**
 A monomorphic instance of array.nested_from_fn
 with const generics
 - K= 4
 */
-void array_nested_from_fn_ac(size_t ret[4U][4U]);
+Eurydice_arr_11 array_nested_from_fn_ac(void);
+
+/**
+A monomorphic instance of array.const_eq
+with const generics
+- K= 2
+*/
+bool array_const_eq_fd(Eurydice_arr_b2 x, Eurydice_arr_b2 y);
 
 void array_main(void);
 
diff --git a/out/test-array2d/array2d.c b/out/test-array2d/array2d.c
index be4b87b3..e513964b 100644
--- a/out/test-array2d/array2d.c
+++ b/out/test-array2d/array2d.c
@@ -7,12 +7,20 @@
 
 #include "array2d.h"
 
-bool array2d_f(uint32_t x[4U][2U])
+bool array2d_f(Eurydice_arr_c0 x)
 {
-  x[0U][0U] = 1U;
-  x[0U][1U] = 2U;
-  uint32_t y[4U][2U] = { { 1U, 2U }, { 3U, 4U }, { 1U, 2U }, { 3U, 4U } };
-  return Eurydice_array_eq((size_t)4U, x, y, uint32_t [2U]);
+  x.data[0U] = (KRML_CLITERAL(Eurydice_arr_b2){ .data = { 1U, 2U } });
+  Eurydice_arr_c0
+  y =
+    {
+      .data = {
+        (KRML_CLITERAL(Eurydice_arr_b2){ .data = { 1U, 2U } }),
+        (KRML_CLITERAL(Eurydice_arr_b2){ .data = { 3U, 4U } }),
+        (KRML_CLITERAL(Eurydice_arr_b2){ .data = { 1U, 2U } }),
+        (KRML_CLITERAL(Eurydice_arr_b2){ .data = { 3U, 4U } })
+      }
+    };
+  return Eurydice_array_eq((size_t)4U, &x, &y, Eurydice_arr_b2);
 }
 
 typedef struct _bool__x2_s
@@ -24,23 +32,19 @@ _bool__x2;
 
 void array2d_main(void)
 {
-  uint32_t y[4U][2U];
+  Eurydice_arr_c0 y;
+  Eurydice_arr_b2 repeat_expression[4U];
   KRML_MAYBE_FOR4(i,
     (size_t)0U,
     (size_t)4U,
     (size_t)1U,
-    y[i][0U] = 1U;
-    y[i][1U] = 2U;);
-  y[1U][0U] = 3U;
-  y[1U][1U] = 4U;
-  y[3U][0U] = 3U;
-  y[3U][1U] = 4U;
-  /* Passing arrays by value in Rust generates a copy in C */
-  uint32_t copy_of_y[4U][2U];
-  memcpy(copy_of_y, y, (size_t)4U * sizeof (uint32_t [2U]));
-  bool actual = array2d_f(copy_of_y);
+    repeat_expression[i] = (KRML_CLITERAL(Eurydice_arr_b2){ .data = { 1U, 2U } }););
+  memcpy(y.data, repeat_expression, (size_t)4U * sizeof (Eurydice_arr_b2));
+  y.data[1U] = (KRML_CLITERAL(Eurydice_arr_b2){ .data = { 3U, 4U } });
+  y.data[3U] = (KRML_CLITERAL(Eurydice_arr_b2){ .data = { 3U, 4U } });
+  bool actual = array2d_f(y);
   bool expected = true;
-  _bool__x2 uu____1 = { .fst = &actual, .snd = &expected };
-  EURYDICE_ASSERT(uu____1.fst[0U] == uu____1.snd[0U], "panic!");
+  _bool__x2 uu____0 = { .fst = &actual, .snd = &expected };
+  EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
 }
 
diff --git a/out/test-array2d/array2d.h b/out/test-array2d/array2d.h
index 9cbd6376..e53051bf 100644
--- a/out/test-array2d/array2d.h
+++ b/out/test-array2d/array2d.h
@@ -19,7 +19,23 @@ extern bool core_cmp_impls__core__cmp__PartialEq_u32__for_u32__eq(uint32_t *x0,
 
 extern bool core_cmp_impls__core__cmp__PartialEq_u32__for_u32__ne(uint32_t *x0, uint32_t *x1);
 
-bool array2d_f(uint32_t x[4U][2U]);
+/**
+A monomorphic instance of Eurydice.arr
+with types uint32_t
+with const generics
+- $2size_t
+*/
+typedef struct Eurydice_arr_b2_s { uint32_t data[2U]; } Eurydice_arr_b2;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr uint32_t[[$2size_t]]
+with const generics
+- $4size_t
+*/
+typedef struct Eurydice_arr_c0_s { Eurydice_arr_b2 data[4U]; } Eurydice_arr_c0;
+
+bool array2d_f(Eurydice_arr_c0 x);
 
 #define core_panicking_AssertKind_Eq 0
 #define core_panicking_AssertKind_Ne 1
diff --git a/out/test-castunsize/castunsize.c b/out/test-castunsize/castunsize.c
new file mode 100644
index 00000000..6736f183
--- /dev/null
+++ b/out/test-castunsize/castunsize.c
@@ -0,0 +1,108 @@
+/* 
+  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
+
+  F* version: <unknown>
+
+ */
+
+#include "castunsize.h"
+
+typedef struct _uint32_t__x2_s
+{
+  uint32_t *fst;
+  uint32_t *snd;
+}
+_uint32_t__x2;
+
+void castunsize_main1(void)
+{
+  castunsize_S_64 x = { .foo = 0U, .my_data = { .data = { 0U } } };
+  Eurydice_dst_da x0 = { .ptr = (castunsize_T *)&x, .len = (size_t)4U };
+  /* original Rust expression is not an lvalue in C */
+  uint32_t lvalue = 0U;
+  _uint32_t__x2
+  uu____0 =
+    {
+      .fst = &Eurydice_slice_index(Eurydice_slice_of_dst(&x0.ptr->my_data,
+          x0.len,
+          uint32_t,
+          Eurydice_slice),
+        (size_t)3U,
+        uint32_t,
+        uint32_t *),
+      .snd = &lvalue
+    };
+  EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
+}
+
+void castunsize_main3(void)
+{
+  Eurydice_slice
+  x =
+    Eurydice_array_to_slice((size_t)4U,
+      Eurydice_box_new((KRML_CLITERAL(Eurydice_arr_0d){ .data = { 0U, 0U, 0U, 0U } }),
+        Eurydice_arr_0d,
+        Eurydice_arr_0d *),
+      uint32_t);
+  /* original Rust expression is not an lvalue in C */
+  uint32_t lvalue = 0U;
+  _uint32_t__x2
+  uu____0 = { .fst = &Eurydice_slice_index(x, (size_t)3U, uint32_t, uint32_t *), .snd = &lvalue };
+  EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
+}
+
+/**
+A monomorphic instance of castunsize.main2
+with const generics
+- K= 5
+*/
+void castunsize_main2_c9(void)
+{
+  castunsize_S_dd x = { .foo = 0U, .my_data = { .data = { 0U } } };
+  Eurydice_dst_da x0 = { .ptr = (castunsize_T *)&x, .len = (size_t)5U };
+  /* original Rust expression is not an lvalue in C */
+  uint32_t lvalue = 0U;
+  _uint32_t__x2
+  uu____0 =
+    {
+      .fst = &Eurydice_slice_index(Eurydice_slice_of_dst(&x0.ptr->my_data,
+          x0.len,
+          uint32_t,
+          Eurydice_slice),
+        (size_t)3U,
+        uint32_t,
+        uint32_t *),
+      .snd = &lvalue
+    };
+  EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
+}
+
+/**
+A monomorphic instance of castunsize.main4
+with const generics
+- K= 5
+*/
+void castunsize_main4_c9(void)
+{
+  Eurydice_slice
+  x =
+    Eurydice_array_to_slice((size_t)5U,
+      Eurydice_box_new((KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 0U, 0U, 0U, 0U } }),
+        Eurydice_arr_88,
+        Eurydice_arr_88 *),
+      uint32_t);
+  /* original Rust expression is not an lvalue in C */
+  uint32_t lvalue = 0U;
+  _uint32_t__x2
+  uu____0 = { .fst = &Eurydice_slice_index(x, (size_t)3U, uint32_t, uint32_t *), .snd = &lvalue };
+  EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
+}
+
+void castunsize_main(void)
+{
+  castunsize_main1();
+  castunsize_main2_c9();
+  castunsize_main3();
+  castunsize_main4_c9();
+}
+
diff --git a/out/test-castunsize/castunsize.h b/out/test-castunsize/castunsize.h
new file mode 100644
index 00000000..ea59f086
--- /dev/null
+++ b/out/test-castunsize/castunsize.h
@@ -0,0 +1,108 @@
+/* 
+  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
+
+  F* version: <unknown>
+
+ */
+
+#ifndef castunsize_H
+#define castunsize_H
+
+#include "eurydice_glue.h"
+
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+typedef struct castunsize_T_s
+{
+  uint32_t foo;
+  uint32_t my_data[];
+}
+castunsize_T;
+
+#define core_panicking_AssertKind_Eq 0
+#define core_panicking_AssertKind_Ne 1
+#define core_panicking_AssertKind_Match 2
+
+typedef uint8_t core_panicking_AssertKind;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types uint32_t
+with const generics
+- $4size_t
+*/
+typedef struct Eurydice_arr_0d_s { uint32_t data[4U]; } Eurydice_arr_0d;
+
+/**
+A monomorphic instance of castunsize.S
+with types Eurydice_arr uint32_t[[$4size_t]]
+
+*/
+typedef struct castunsize_S_64_s
+{
+  uint32_t foo;
+  Eurydice_arr_0d my_data;
+}
+castunsize_S_64;
+
+/**
+A monomorphic instance of Eurydice.dst
+with types castunsize_S Eurydice_derefed_slice uint32_t
+
+*/
+typedef struct Eurydice_dst_da_s
+{
+  castunsize_T *ptr;
+  size_t len;
+}
+Eurydice_dst_da;
+
+void castunsize_main1(void);
+
+void castunsize_main3(void);
+
+/**
+A monomorphic instance of Eurydice.arr
+with types uint32_t
+with const generics
+- $5size_t
+*/
+typedef struct Eurydice_arr_88_s { uint32_t data[5U]; } Eurydice_arr_88;
+
+/**
+A monomorphic instance of castunsize.S
+with types Eurydice_arr uint32_t[[$5size_t]]
+
+*/
+typedef struct castunsize_S_dd_s
+{
+  uint32_t foo;
+  Eurydice_arr_88 my_data;
+}
+castunsize_S_dd;
+
+/**
+A monomorphic instance of castunsize.main2
+with const generics
+- K= 5
+*/
+void castunsize_main2_c9(void);
+
+/**
+A monomorphic instance of castunsize.main4
+with const generics
+- K= 5
+*/
+void castunsize_main4_c9(void);
+
+void castunsize_main(void);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define castunsize_H_DEFINED
+#endif /* castunsize_H */
diff --git a/out/test-const_generics/const_generics.c b/out/test-const_generics/const_generics.c
index 907464ed..1a40620d 100644
--- a/out/test-const_generics/const_generics.c
+++ b/out/test-const_generics/const_generics.c
@@ -14,41 +14,45 @@ A monomorphic instance of const_generics.serialize
 with const generics
 - OUT_LEN= 8
 */
-void const_generics_serialize_3b(Eurydice_slice re, uint8_t ret[8U])
+Eurydice_arr_c4 const_generics_serialize_3b(Eurydice_slice re)
 {
-  uint8_t out[8U] = { 0U };
+  Eurydice_arr_c4 out = { .data = { 0U } };
   Eurydice_slice
   uu____0 =
     Eurydice_array_to_subslice_to((size_t)8U,
-      out,
+      &out,
       (size_t)4U,
       uint8_t,
       size_t,
       uint8_t []);
-  uint8_t ret0[4U];
-  core_num__u32__to_be_bytes(Eurydice_slice_index(re, (size_t)0U, uint32_t, uint32_t *), ret0);
-  Eurydice_slice_copy(uu____0, Eurydice_array_to_slice((size_t)4U, ret0, uint8_t), uint8_t);
+  /* original Rust expression is not an lvalue in C */
+  Eurydice_arr_e9
+  lvalue0 =
+    core_num__u32__to_be_bytes(Eurydice_slice_index(re, (size_t)0U, uint32_t, uint32_t *));
+  Eurydice_slice_copy(uu____0, Eurydice_array_to_slice((size_t)4U, &lvalue0, uint8_t), uint8_t);
   Eurydice_slice
   uu____1 =
     Eurydice_array_to_subslice_from((size_t)8U,
-      out,
+      &out,
       (size_t)4U,
       uint8_t,
       size_t,
       uint8_t []);
-  uint8_t ret1[4U];
-  core_num__u32__to_be_bytes(Eurydice_slice_index(re, (size_t)1U, uint32_t, uint32_t *), ret1);
-  Eurydice_slice_copy(uu____1, Eurydice_array_to_slice((size_t)4U, ret1, uint8_t), uint8_t);
-  memcpy(ret, out, (size_t)8U * sizeof (uint8_t));
+  /* original Rust expression is not an lvalue in C */
+  Eurydice_arr_e9
+  lvalue = core_num__u32__to_be_bytes(Eurydice_slice_index(re, (size_t)1U, uint32_t, uint32_t *));
+  Eurydice_slice_copy(uu____1, Eurydice_array_to_slice((size_t)4U, &lvalue, uint8_t), uint8_t);
+  return out;
 }
 
 void const_generics_main(void)
 {
-  uint8_t s[8U];
-  uint32_t buf[2U] = { 1U, 2U };
-  const_generics_serialize_3b(Eurydice_array_to_slice((size_t)2U, buf, uint32_t), s);
-  EURYDICE_ASSERT(s[3U] == 1U, "panic!");
-  EURYDICE_ASSERT(s[7U] == 2U, "panic!");
+  /* original Rust expression is not an lvalue in C */
+  Eurydice_arr_b2 lvalue = { .data = { 1U, 2U } };
+  Eurydice_arr_c4
+  s = const_generics_serialize_3b(Eurydice_array_to_slice((size_t)2U, &lvalue, uint32_t));
+  EURYDICE_ASSERT(s.data[3U] == 1U, "panic!");
+  EURYDICE_ASSERT(s.data[7U] == 2U, "panic!");
 }
 
 /**
@@ -60,36 +64,17 @@ with const generics
 */
 const_generics_Pair_4e const_generics_mk_pairs_e0(uint32_t x, uint64_t y)
 {
-  uint32_t a1[2U];
-  KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, a1[i] = x;);
-  uint64_t a2[4U];
-  KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, a2[i] = y;);
-  /* Passing arrays by value in Rust generates a copy in C */
-  uint32_t copy_of_a10[2U];
-  memcpy(copy_of_a10, a1, (size_t)2U * sizeof (uint32_t));
-  /* Passing arrays by value in Rust generates a copy in C */
-  uint64_t copy_of_a20[4U];
-  memcpy(copy_of_a20, a2, (size_t)4U * sizeof (uint64_t));
-  const_generics_Pair_a5 p1;
-  memcpy(p1.left, copy_of_a10, (size_t)2U * sizeof (uint32_t));
-  memcpy(p1.right, copy_of_a20, (size_t)4U * sizeof (uint64_t));
-  /* Passing arrays by value in Rust generates a copy in C */
-  uint64_t copy_of_a2[4U];
-  memcpy(copy_of_a2, a2, (size_t)4U * sizeof (uint64_t));
-  /* Passing arrays by value in Rust generates a copy in C */
-  uint32_t copy_of_a1[2U];
-  memcpy(copy_of_a1, a1, (size_t)2U * sizeof (uint32_t));
-  const_generics_Pair_87 p2;
-  memcpy(p2.left, copy_of_a2, (size_t)4U * sizeof (uint64_t));
-  memcpy(p2.right, copy_of_a1, (size_t)2U * sizeof (uint32_t));
-  uint32_t uu____4[2U];
-  memcpy(uu____4, p1.left, (size_t)2U * sizeof (uint32_t));
-  uint32_t uu____5[2U];
-  memcpy(uu____5, p2.right, (size_t)2U * sizeof (uint32_t));
-  const_generics_Pair_4e lit;
-  memcpy(lit.left, uu____4, (size_t)2U * sizeof (uint32_t));
-  memcpy(lit.right, uu____5, (size_t)2U * sizeof (uint32_t));
-  return lit;
+  Eurydice_arr_b2 a1;
+  uint32_t repeat_expression0[2U];
+  KRML_MAYBE_FOR2(i, (size_t)0U, (size_t)2U, (size_t)1U, repeat_expression0[i] = x;);
+  memcpy(a1.data, repeat_expression0, (size_t)2U * sizeof (uint32_t));
+  Eurydice_arr_61 a2;
+  uint64_t repeat_expression[4U];
+  KRML_MAYBE_FOR4(i, (size_t)0U, (size_t)4U, (size_t)1U, repeat_expression[i] = y;);
+  memcpy(a2.data, repeat_expression, (size_t)4U * sizeof (uint64_t));
+  const_generics_Pair_a5 p1 = { .left = a1, .right = a2 };
+  const_generics_Pair_87 p2 = { .left = a2, .right = a1 };
+  return (KRML_CLITERAL(const_generics_Pair_4e){ .left = p1.left, .right = p2.right });
 }
 
 typedef struct _uint32_t__x2_s
@@ -102,18 +87,16 @@ _uint32_t__x2;
 void const_generics_main1(void)
 {
   const_generics_Pair_4e uu____0 = const_generics_mk_pairs_e0(0U, 0ULL);
-  uint32_t left[2U];
-  memcpy(left, uu____0.left, (size_t)2U * sizeof (uint32_t));
-  uint32_t right[2U];
-  memcpy(right, uu____0.right, (size_t)2U * sizeof (uint32_t));
+  Eurydice_arr_b2 left = uu____0.left;
+  Eurydice_arr_b2 right = uu____0.right;
   uint32_t expected = 0U;
-  _uint32_t__x2 uu____1 = { .fst = left, .snd = &expected };
+  _uint32_t__x2 uu____1 = { .fst = left.data, .snd = &expected };
   EURYDICE_ASSERT(uu____1.fst[0U] == uu____1.snd[0U], "panic!");
-  _uint32_t__x2 uu____2 = { .fst = &left[1U], .snd = &expected };
+  _uint32_t__x2 uu____2 = { .fst = &left.data[1U], .snd = &expected };
   EURYDICE_ASSERT(uu____2.fst[0U] == uu____2.snd[0U], "panic!");
-  _uint32_t__x2 uu____3 = { .fst = right, .snd = &expected };
+  _uint32_t__x2 uu____3 = { .fst = right.data, .snd = &expected };
   EURYDICE_ASSERT(uu____3.fst[0U] == uu____3.snd[0U], "panic!");
-  _uint32_t__x2 uu____4 = { .fst = &right[1U], .snd = &expected };
+  _uint32_t__x2 uu____4 = { .fst = &right.data[1U], .snd = &expected };
   EURYDICE_ASSERT(uu____4.fst[0U] == uu____4.snd[0U], "panic!");
 }
 
@@ -125,18 +108,22 @@ with const generics
 */
 bool const_generics_f_e5(uint32_t x, size_t y)
 {
-  uint32_t arr1[1U];
+  Eurydice_arr_a5 arr1;
+  uint32_t repeat_expression0[1U];
   {
-    arr1[0U] = x;
+    repeat_expression0[0U] = x;
   }
-  size_t arr2[1U];
+  memcpy(arr1.data, repeat_expression0, (size_t)1U * sizeof (uint32_t));
+  Eurydice_arr_e4 arr2;
+  size_t repeat_expression[1U];
   {
-    arr2[0U] = y;
+    repeat_expression[0U] = y;
   }
+  memcpy(arr2.data, repeat_expression, (size_t)1U * sizeof (size_t));
   bool uu____0;
-  if (arr1[0U] == 2U)
+  if (arr1.data[0U] == 2U)
   {
-    uu____0 = arr2[0U] == (size_t)1U;
+    uu____0 = arr2.data[0U] == (size_t)1U;
   }
   else
   {
@@ -153,14 +140,18 @@ with const generics
 */
 bool const_generics_f_70(uint32_t x, size_t y)
 {
-  uint32_t arr1[3U];
-  KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, arr1[i] = x;);
-  size_t arr2[3U];
-  KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, arr2[i] = y;);
+  Eurydice_arr_6f arr1;
+  uint32_t repeat_expression0[3U];
+  KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, repeat_expression0[i] = x;);
+  memcpy(arr1.data, repeat_expression0, (size_t)3U * sizeof (uint32_t));
+  Eurydice_arr_c8 arr2;
+  size_t repeat_expression[3U];
+  KRML_MAYBE_FOR3(i, (size_t)0U, (size_t)3U, (size_t)1U, repeat_expression[i] = y;);
+  memcpy(arr2.data, repeat_expression, (size_t)3U * sizeof (size_t));
   bool uu____0;
-  if (arr1[0U] == 4U)
+  if (arr1.data[0U] == 4U)
   {
-    uu____0 = arr2[0U] == (size_t)3U;
+    uu____0 = arr2.data[0U] == (size_t)3U;
   }
   else
   {
diff --git a/out/test-const_generics/const_generics.h b/out/test-const_generics/const_generics.h
index 54340c09..953869d3 100644
--- a/out/test-const_generics/const_generics.h
+++ b/out/test-const_generics/const_generics.h
@@ -15,14 +15,22 @@
 extern "C" {
 #endif
 
-static inline void core_num__u32__to_be_bytes(uint32_t x0, uint8_t x1[4U]);
+static inline Eurydice_arr_e9 core_num__u32__to_be_bytes(uint32_t x0);
 
 /**
 A monomorphic instance of const_generics.serialize
 with const generics
 - OUT_LEN= 8
 */
-void const_generics_serialize_3b(Eurydice_slice re, uint8_t ret[8U]);
+Eurydice_arr_c4 const_generics_serialize_3b(Eurydice_slice re);
+
+/**
+A monomorphic instance of Eurydice.arr
+with types uint32_t
+with const generics
+- $2size_t
+*/
+typedef struct Eurydice_arr_b2_s { uint32_t data[2U]; } Eurydice_arr_b2;
 
 void const_generics_main(void);
 
@@ -41,11 +49,19 @@ with const generics
 */
 typedef struct const_generics_Pair_4e_s
 {
-  uint32_t left[2U];
-  uint32_t right[2U];
+  Eurydice_arr_b2 left;
+  Eurydice_arr_b2 right;
 }
 const_generics_Pair_4e;
 
+/**
+A monomorphic instance of Eurydice.arr
+with types uint64_t
+with const generics
+- $4size_t
+*/
+typedef struct Eurydice_arr_61_s { uint64_t data[4U]; } Eurydice_arr_61;
+
 /**
 A monomorphic instance of const_generics.Pair
 with types uint32_t, uint64_t
@@ -55,8 +71,8 @@ with const generics
 */
 typedef struct const_generics_Pair_a5_s
 {
-  uint32_t left[2U];
-  uint64_t right[4U];
+  Eurydice_arr_b2 left;
+  Eurydice_arr_61 right;
 }
 const_generics_Pair_a5;
 
@@ -69,8 +85,8 @@ with const generics
 */
 typedef struct const_generics_Pair_87_s
 {
-  uint64_t left[4U];
-  uint32_t right[2U];
+  Eurydice_arr_61 left;
+  Eurydice_arr_b2 right;
 }
 const_generics_Pair_87;
 
@@ -85,6 +101,22 @@ const_generics_Pair_4e const_generics_mk_pairs_e0(uint32_t x, uint64_t y);
 
 void const_generics_main1(void);
 
+/**
+A monomorphic instance of Eurydice.arr
+with types uint32_t
+with const generics
+- $1size_t
+*/
+typedef struct Eurydice_arr_a5_s { uint32_t data[1U]; } Eurydice_arr_a5;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types size_t
+with const generics
+- $1size_t
+*/
+typedef struct Eurydice_arr_e4_s { size_t data[1U]; } Eurydice_arr_e4;
+
 /**
 A monomorphic instance of const_generics.f
 with const generics
@@ -93,6 +125,22 @@ with const generics
 */
 bool const_generics_f_e5(uint32_t x, size_t y);
 
+/**
+A monomorphic instance of Eurydice.arr
+with types uint32_t
+with const generics
+- $3size_t
+*/
+typedef struct Eurydice_arr_6f_s { uint32_t data[3U]; } Eurydice_arr_6f;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types size_t
+with const generics
+- $3size_t
+*/
+typedef struct Eurydice_arr_c8_s { size_t data[3U]; } Eurydice_arr_c8;
+
 /**
 A monomorphic instance of const_generics.f
 with const generics
diff --git a/out/test-dst/dst.c b/out/test-dst/dst.c
index 33e38990..46d715c1 100644
--- a/out/test-dst/dst.c
+++ b/out/test-dst/dst.c
@@ -13,28 +13,35 @@ Eurydice_dst_31 dst_alloc(void)
     (
       KRML_CLITERAL(Eurydice_dst_31){
         .ptr = (dst_T *)Eurydice_box_new((
-            KRML_CLITERAL(dst_S_dd){ .foo = 0U, .my_data = { 0U, 0U, 0U, 0U } }
+            KRML_CLITERAL(dst_S_64){ .foo = 0U, .my_data = { .data = { 0U, 0U, 0U, 0U } } }
           ),
-          dst_S_dd,
-          dst_S_dd *),
+          dst_S_64,
+          dst_S_64 *),
         .len = (size_t)4U
       }
     );
 }
 
-Eurydice_dst_f1 dst_alloc3(void)
+Eurydice_dst_40 dst_alloc3(void)
 {
   return
     (
-      KRML_CLITERAL(Eurydice_dst_f1){
+      KRML_CLITERAL(Eurydice_dst_40){
         .ptr = (dst_T3 *)Eurydice_box_new((
-            KRML_CLITERAL(dst_S_a4){
+            KRML_CLITERAL(dst_S_9c){
               .foo = 0U,
-              .my_data = { { 0U, 0U, 0U }, { 0U, 0U, 0U }, { 0U, 0U, 0U }, { 0U, 0U, 0U } }
+              .my_data = {
+                .data = {
+                  (KRML_CLITERAL(Eurydice_arr_6f){ .data = { 0U, 0U, 0U } }),
+                  (KRML_CLITERAL(Eurydice_arr_6f){ .data = { 0U, 0U, 0U } }),
+                  (KRML_CLITERAL(Eurydice_arr_6f){ .data = { 0U, 0U, 0U } }),
+                  (KRML_CLITERAL(Eurydice_arr_6f){ .data = { 0U, 0U, 0U } })
+                }
+              }
             }
           ),
-          dst_S_a4,
-          dst_S_a4 *),
+          dst_S_9c,
+          dst_S_9c *),
         .len = (size_t)4U
       }
     );
@@ -101,7 +108,7 @@ void dst_check_var_field_ref(Eurydice_dst_31 x)
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
 }
 
-void dst_check_var_field_ref3(Eurydice_dst_f1 x)
+void dst_check_var_field_ref3(Eurydice_dst_40 x)
 {
   /* original Rust expression is not an lvalue in C */
   uint32_t lvalue = 0U;
@@ -110,11 +117,11 @@ void dst_check_var_field_ref3(Eurydice_dst_f1 x)
     {
       .fst = Eurydice_slice_index(Eurydice_slice_of_dst(&x.ptr->my_data,
           x.len,
-          uint32_t [3U],
+          Eurydice_arr_6f,
           Eurydice_slice),
         (size_t)0U,
-        uint32_t [3U],
-        uint32_t (*)[3U]),
+        Eurydice_arr_6f,
+        Eurydice_arr_6f *).data,
       .snd = &lvalue
     };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
@@ -122,28 +129,28 @@ void dst_check_var_field_ref3(Eurydice_dst_f1 x)
 
 void dst_main3(void)
 {
-  Eurydice_dst_f1 x = dst_alloc3();
+  Eurydice_dst_40 x = dst_alloc3();
   dst_check_var_field_ref3(x);
 }
 
 Eurydice_dst_7a dst_mk(void)
 {
-  dst_T2_dd x = { .header = (size_t)0U, .my_data = { 0U } };
-  x.my_data[1U] = 2U;
+  dst_T2_64 x = { .header = (size_t)0U, .my_data = { .data = { 0U } } };
+  x.my_data.data[1U] = 2U;
   Eurydice_dst_7a
-  y = { .ptr = (dst_T2_be *)Eurydice_box_new(x, dst_T2_dd, dst_T2_dd *), .len = (size_t)4U };
+  y = { .ptr = (dst_T2_be *)Eurydice_box_new(x, dst_T2_64, dst_T2_64 *), .len = (size_t)4U };
   return y;
 }
 
 void dst_main4(void)
 {
-  uint32_t buf[4U] = { 0U };
   Eurydice_slice
   x =
-    Eurydice_slice_of_boxed_array(Eurydice_box_new_array((size_t)4U, buf, uint32_t, uint32_t *),
-      (size_t)4U,
-      uint32_t,
-      Eurydice_slice);
+    Eurydice_array_to_slice((size_t)4U,
+      Eurydice_box_new((KRML_CLITERAL(Eurydice_arr_0d){ .data = { 0U, 0U, 0U, 0U } }),
+        Eurydice_arr_0d,
+        Eurydice_arr_0d *),
+      uint32_t);
   /* original Rust expression is not an lvalue in C */
   uint32_t lvalue = 0U;
   _uint32_t__x2
@@ -155,7 +162,7 @@ void dst_main(void)
 {
   dst_check_regular_field(dst_alloc());
   dst_check_var_field(dst_alloc());
-  dst_S_dd x = { .foo = 0U, .my_data = { 0U } };
+  dst_S_64 x = { .foo = 0U, .my_data = { .data = { 0U } } };
   Eurydice_dst_31 x0 = { .ptr = (dst_T *)&x, .len = (size_t)4U };
   dst_check_regular_field_ref(x0);
   dst_check_var_field_ref(x0);
diff --git a/out/test-dst/dst.h b/out/test-dst/dst.h
index 76573f0d..fa2f46da 100644
--- a/out/test-dst/dst.h
+++ b/out/test-dst/dst.h
@@ -28,10 +28,18 @@ typedef struct dst_T_s
 }
 dst_T;
 
+/**
+A monomorphic instance of Eurydice.arr
+with types uint32_t
+with const generics
+- $3size_t
+*/
+typedef struct Eurydice_arr_6f_s { uint32_t data[3U]; } Eurydice_arr_6f;
+
 typedef struct dst_T3_s
 {
   uint32_t foo;
-  uint32_t my_data[][3U];
+  Eurydice_arr_6f my_data[];
 }
 dst_T3;
 
@@ -47,45 +55,61 @@ typedef struct Eurydice_dst_31_s
 }
 Eurydice_dst_31;
 
+/**
+A monomorphic instance of Eurydice.arr
+with types uint32_t
+with const generics
+- $4size_t
+*/
+typedef struct Eurydice_arr_0d_s { uint32_t data[4U]; } Eurydice_arr_0d;
+
 /**
 A monomorphic instance of dst.S
-with types uint32_t[4size_t]
+with types Eurydice_arr uint32_t[[$4size_t]]
 
 */
-typedef struct dst_S_dd_s
+typedef struct dst_S_64_s
 {
   uint32_t foo;
-  uint32_t my_data[4U];
+  Eurydice_arr_0d my_data;
 }
-dst_S_dd;
+dst_S_64;
 
 Eurydice_dst_31 dst_alloc(void);
 
 /**
 A monomorphic instance of Eurydice.dst
-with types dst_S Eurydice_derefed_slice uint32_t[3size_t]
+with types dst_S Eurydice_derefed_slice Eurydice_arr uint32_t[[$3size_t]]
 
 */
-typedef struct Eurydice_dst_f1_s
+typedef struct Eurydice_dst_40_s
 {
   dst_T3 *ptr;
   size_t len;
 }
-Eurydice_dst_f1;
+Eurydice_dst_40;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr uint32_t[[$3size_t]]
+with const generics
+- $4size_t
+*/
+typedef struct Eurydice_arr_58_s { Eurydice_arr_6f data[4U]; } Eurydice_arr_58;
 
 /**
 A monomorphic instance of dst.S
-with types uint32_t[3size_t][4size_t]
+with types Eurydice_arr Eurydice_arr uint32_t[[$3size_t]][[$4size_t]]
 
 */
-typedef struct dst_S_a4_s
+typedef struct dst_S_9c_s
 {
   uint32_t foo;
-  uint32_t my_data[4U][3U];
+  Eurydice_arr_58 my_data;
 }
-dst_S_a4;
+dst_S_9c;
 
-Eurydice_dst_f1 dst_alloc3(void);
+Eurydice_dst_40 dst_alloc3(void);
 
 void dst_check_regular_field(Eurydice_dst_31 x);
 
@@ -95,7 +119,7 @@ void dst_check_var_field(Eurydice_dst_31 x);
 
 void dst_check_var_field_ref(Eurydice_dst_31 x);
 
-void dst_check_var_field_ref3(Eurydice_dst_f1 x);
+void dst_check_var_field_ref3(Eurydice_dst_40 x);
 
 void dst_main3(void);
 
@@ -125,15 +149,15 @@ Eurydice_dst_7a;
 
 /**
 A monomorphic instance of dst.T2
-with types uint32_t[4size_t]
+with types Eurydice_arr uint32_t[[$4size_t]]
 
 */
-typedef struct dst_T2_dd_s
+typedef struct dst_T2_64_s
 {
   size_t header;
-  uint32_t my_data[4U];
+  Eurydice_arr_0d my_data;
 }
-dst_T2_dd;
+dst_T2_64;
 
 Eurydice_dst_7a dst_mk(void);
 
diff --git a/out/test-floating_points/floating_points.c b/out/test-floating_points/floating_points.c
index a3c79a90..04d7c7d5 100644
--- a/out/test-floating_points/floating_points.c
+++ b/out/test-floating_points/floating_points.c
@@ -31,35 +31,41 @@ _size_t__x2;
 void floating_points_main(void)
 {
   float32_t f = (float32_t)1;
-  float32_t arr[100U];
+  Eurydice_arr_d5 arr;
+  float32_t repeat_expression0[100U];
   for (size_t i = (size_t)0U; i < (size_t)100U; i++)
   {
-    arr[i] = f;
+    repeat_expression0[i] = f;
   }
+  memcpy(arr.data, repeat_expression0, (size_t)100U * sizeof (float32_t));
   float64_t d = (float64_t)1;
-  float64_t arr2[100U];
+  Eurydice_arr_22 arr2;
+  float64_t repeat_expression[100U];
   for (size_t i = (size_t)0U; i < (size_t)100U; i++)
   {
-    arr2[i] = d;
+    repeat_expression[i] = d;
   }
+  memcpy(arr2.data, repeat_expression, (size_t)100U * sizeof (float64_t));
   /* original Rust expression is not an lvalue in C */
   float32_t lvalue0 = (float32_t)1;
-  _float32_t__x2 uu____0 = { .fst = arr, .snd = &lvalue0 };
+  _float32_t__x2 uu____0 = { .fst = arr.data, .snd = &lvalue0 };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
   /* original Rust expression is not an lvalue in C */
   float64_t lvalue1 = (float64_t)1;
-  _float64_t__x2 uu____1 = { .fst = arr2, .snd = &lvalue1 };
+  _float64_t__x2 uu____1 = { .fst = arr2.data, .snd = &lvalue1 };
   EURYDICE_ASSERT(uu____1.fst[0U] == uu____1.snd[0U], "panic!");
   /* original Rust expression is not an lvalue in C */
   size_t
-  lvalue2 = Eurydice_slice_len(Eurydice_array_to_slice((size_t)100U, arr, float32_t), float32_t);
+  lvalue2 = Eurydice_slice_len(Eurydice_array_to_slice((size_t)100U, &arr, float32_t), float32_t);
   /* original Rust expression is not an lvalue in C */
   size_t lvalue3 = (size_t)100U;
   _size_t__x2 uu____2 = { .fst = &lvalue2, .snd = &lvalue3 };
   EURYDICE_ASSERT(uu____2.fst[0U] == uu____2.snd[0U], "panic!");
   /* original Rust expression is not an lvalue in C */
   size_t
-  lvalue4 = Eurydice_slice_len(Eurydice_array_to_slice((size_t)100U, arr2, float64_t), float64_t);
+  lvalue4 =
+    Eurydice_slice_len(Eurydice_array_to_slice((size_t)100U, &arr2, float64_t),
+      float64_t);
   /* original Rust expression is not an lvalue in C */
   size_t lvalue = (size_t)100U;
   _size_t__x2 uu____3 = { .fst = &lvalue4, .snd = &lvalue };
diff --git a/out/test-floating_points/floating_points.h b/out/test-floating_points/floating_points.h
index 0e132f8d..e4d37532 100644
--- a/out/test-floating_points/floating_points.h
+++ b/out/test-floating_points/floating_points.h
@@ -21,6 +21,22 @@ extern "C" {
 
 typedef uint8_t core_panicking_AssertKind;
 
+/**
+A monomorphic instance of Eurydice.arr
+with types float32_t
+with const generics
+- $100size_t
+*/
+typedef struct Eurydice_arr_d5_s { float32_t data[100U]; } Eurydice_arr_d5;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types float64_t
+with const generics
+- $100size_t
+*/
+typedef struct Eurydice_arr_22_s { float64_t data[100U]; } Eurydice_arr_22;
+
 void floating_points_main(void);
 
 #if defined(__cplusplus)
diff --git a/out/test-fn_higher_order/fn_higher_order.c b/out/test-fn_higher_order/fn_higher_order.c
index 49b0febc..f73318ef 100644
--- a/out/test-fn_higher_order/fn_higher_order.c
+++ b/out/test-fn_higher_order/fn_higher_order.c
@@ -12,7 +12,7 @@ int32_t fn_higher_order_empty_ptr(int32_t (*f)(void))
   return f();
 }
 
-int32_t fn_higher_order_more_sum_lst(int32_t *l)
+int32_t fn_higher_order_more_sum_lst(Eurydice_arr_8d *l)
 {
   int32_t sum = (int32_t)0;
   KRML_MAYBE_FOR3(i,
@@ -20,7 +20,7 @@ int32_t fn_higher_order_more_sum_lst(int32_t *l)
     (size_t)3U,
     (size_t)1U,
     size_t i0 = i;
-    sum = sum + l[i0];);
+    sum = sum + l->data[i0];);
   return sum;
 }
 
@@ -32,9 +32,9 @@ with const generics
 */
 size_t
 fn_higher_order_compose_cg_apply_fd(
-  size_t (*f)(size_t *x0),
+  size_t (*f)(Eurydice_arr_99 *x0),
   size_t (*g)(size_t x0),
-  size_t *arg
+  Eurydice_arr_99 *arg
 )
 {
   size_t (*uu____0)(size_t x0) = g;
@@ -46,7 +46,7 @@ A monomorphic instance of fn_higher_order.sum_lst
 with const generics
 - N= 5
 */
-size_t fn_higher_order_sum_lst_c9(size_t *lst)
+size_t fn_higher_order_sum_lst_c9(Eurydice_arr_99 *lst)
 {
   size_t sum = (size_t)0U;
   KRML_MAYBE_FOR5(i,
@@ -54,7 +54,7 @@ size_t fn_higher_order_sum_lst_c9(size_t *lst)
     (size_t)5U,
     (size_t)1U,
     size_t i0 = i;
-    sum = sum + lst[i0];);
+    sum = sum + lst->data[i0];);
   return sum + (size_t)5U;
 }
 
@@ -76,9 +76,9 @@ with const generics
 */
 int32_t
 fn_higher_order_compose_cg_apply_82(
-  int32_t (*f)(int32_t *x0),
+  int32_t (*f)(Eurydice_arr_8d *x0),
   int32_t (*g)(int32_t x0),
-  int32_t *arg
+  Eurydice_arr_8d *arg
 )
 {
   int32_t (*uu____0)(int32_t x0) = g;
@@ -111,25 +111,28 @@ _int32_t__x2;
 
 void fn_higher_order_use_compose_cg(void)
 {
-  size_t buf0[5U] = { (size_t)1U, (size_t)2U, (size_t)3U, (size_t)4U, (size_t)5U };
+  /* original Rust expression is not an lvalue in C */
+  Eurydice_arr_99
+  lvalue0 = { .data = { (size_t)1U, (size_t)2U, (size_t)3U, (size_t)4U, (size_t)5U } };
   size_t
   x =
     fn_higher_order_compose_cg_apply_fd(fn_higher_order_sum_lst_c9,
       fn_higher_order_id_37,
-      buf0);
-  int32_t buf[3U] = { (int32_t)10, (int32_t)11, (int32_t)12 };
+      &lvalue0);
+  /* original Rust expression is not an lvalue in C */
+  Eurydice_arr_8d lvalue1 = { .data = { (int32_t)10, (int32_t)11, (int32_t)12 } };
   int32_t
   y =
     fn_higher_order_compose_cg_apply_82(fn_higher_order_more_sum_lst,
       fn_higher_order_id_a8,
-      buf);
+      &lvalue1);
   /* original Rust expression is not an lvalue in C */
   size_t lvalue = (size_t)20U;
   _size_t__x2 uu____0 = { .fst = &x, .snd = &lvalue };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
   /* original Rust expression is not an lvalue in C */
-  int32_t lvalue0 = (int32_t)33;
-  _int32_t__x2 uu____1 = { .fst = &y, .snd = &lvalue0 };
+  int32_t lvalue2 = (int32_t)33;
+  _int32_t__x2 uu____1 = { .fst = &y, .snd = &lvalue2 };
   EURYDICE_ASSERT(uu____1.fst[0U] == uu____1.snd[0U], "panic!");
 }
 
diff --git a/out/test-fn_higher_order/fn_higher_order.h b/out/test-fn_higher_order/fn_higher_order.h
index 1ffd62a7..10338183 100644
--- a/out/test-fn_higher_order/fn_higher_order.h
+++ b/out/test-fn_higher_order/fn_higher_order.h
@@ -88,7 +88,23 @@ typedef uint8_t core_panicking_AssertKind;
 
 int32_t fn_higher_order_empty_ptr(int32_t (*f)(void));
 
-int32_t fn_higher_order_more_sum_lst(int32_t *l);
+/**
+A monomorphic instance of Eurydice.arr
+with types int32_t
+with const generics
+- $3size_t
+*/
+typedef struct Eurydice_arr_8d_s { int32_t data[3U]; } Eurydice_arr_8d;
+
+int32_t fn_higher_order_more_sum_lst(Eurydice_arr_8d *l);
+
+/**
+A monomorphic instance of Eurydice.arr
+with types size_t
+with const generics
+- $5size_t
+*/
+typedef struct Eurydice_arr_99_s { size_t data[5U]; } Eurydice_arr_99;
 
 /**
 A monomorphic instance of fn_higher_order.compose_cg_apply
@@ -98,9 +114,9 @@ with const generics
 */
 size_t
 fn_higher_order_compose_cg_apply_fd(
-  size_t (*f)(size_t *x0),
+  size_t (*f)(Eurydice_arr_99 *x0),
   size_t (*g)(size_t x0),
-  size_t *arg
+  Eurydice_arr_99 *arg
 );
 
 /**
@@ -108,7 +124,7 @@ A monomorphic instance of fn_higher_order.sum_lst
 with const generics
 - N= 5
 */
-size_t fn_higher_order_sum_lst_c9(size_t *lst);
+size_t fn_higher_order_sum_lst_c9(Eurydice_arr_99 *lst);
 
 /**
 A monomorphic instance of fn_higher_order.id
@@ -125,9 +141,9 @@ with const generics
 */
 int32_t
 fn_higher_order_compose_cg_apply_82(
-  int32_t (*f)(int32_t *x0),
+  int32_t (*f)(Eurydice_arr_8d *x0),
   int32_t (*g)(int32_t x0),
-  int32_t *arg
+  Eurydice_arr_8d *arg
 );
 
 /**
diff --git a/out/test-issue_128/issue_128.c b/out/test-issue_128/issue_128.c
index e8e409a6..ab3d822c 100644
--- a/out/test-issue_128/issue_128.c
+++ b/out/test-issue_128/issue_128.c
@@ -40,7 +40,9 @@ void issue_128_use_enum(issue_128_E e, Eurydice_slice x)
 
 void issue_128_main(void)
 {
-  uint8_t buf[0U] = {  };
-  issue_128_use_enum(issue_128_E_A, Eurydice_array_to_slice((size_t)0U, buf, uint8_t));
+  issue_128_E uu____0 = issue_128_E_A;
+  /* original Rust expression is not an lvalue in C */
+  Eurydice_arr_51 lvalue = Eurydice_empty_array((void *)0U, uint8_t, Eurydice_arr_51);
+  issue_128_use_enum(uu____0, Eurydice_array_to_slice((size_t)0U, &lvalue, uint8_t));
 }
 
diff --git a/out/test-issue_128/issue_128.h b/out/test-issue_128/issue_128.h
index 7739658f..0a872ac2 100644
--- a/out/test-issue_128/issue_128.h
+++ b/out/test-issue_128/issue_128.h
@@ -26,6 +26,14 @@ void issue_128_fun_b(Eurydice_slice _x);
 
 void issue_128_use_enum(issue_128_E e, Eurydice_slice x);
 
+/**
+A monomorphic instance of Eurydice.arr
+with types uint8_t
+with const generics
+- $0size_t
+*/
+typedef struct Eurydice_arr_51_s { uint8_t data[0U]; } Eurydice_arr_51;
+
 void issue_128_main(void);
 
 #if defined(__cplusplus)
diff --git a/out/test-issue_212/issue_212.c b/out/test-issue_212/issue_212.c
new file mode 100644
index 00000000..f4407688
--- /dev/null
+++ b/out/test-issue_212/issue_212.c
@@ -0,0 +1,26 @@
+/* 
+  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
+
+  F* version: <unknown>
+
+ */
+
+#include "issue_212.h"
+
+/**
+A monomorphic instance of issue_212.id_mut
+with types Eurydice_arr int32_t[[$3size_t]]
+
+*/
+Eurydice_arr_8d *issue_212_id_mut_16(Eurydice_arr_8d *x)
+{
+  return x;
+}
+
+void issue_212_main(void)
+{
+  Eurydice_arr_8d arr = { .data = { (int32_t)1, (int32_t)2, (int32_t)3 } };
+  Eurydice_arr_8d *r = issue_212_id_mut_16(&arr);
+  EURYDICE_ASSERT(r->data[0U] > (int32_t)0, "panic!");
+}
+
diff --git a/out/test-issue_212/issue_212.h b/out/test-issue_212/issue_212.h
new file mode 100644
index 00000000..7dc5f135
--- /dev/null
+++ b/out/test-issue_212/issue_212.h
@@ -0,0 +1,40 @@
+/* 
+  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
+
+  F* version: <unknown>
+
+ */
+
+#ifndef issue_212_H
+#define issue_212_H
+
+#include "eurydice_glue.h"
+
+
+#if defined(__cplusplus)
+extern "C" {
+#endif
+
+/**
+A monomorphic instance of Eurydice.arr
+with types int32_t
+with const generics
+- $3size_t
+*/
+typedef struct Eurydice_arr_8d_s { int32_t data[3U]; } Eurydice_arr_8d;
+
+/**
+A monomorphic instance of issue_212.id_mut
+with types Eurydice_arr int32_t[[$3size_t]]
+
+*/
+Eurydice_arr_8d *issue_212_id_mut_16(Eurydice_arr_8d *x);
+
+void issue_212_main(void);
+
+#if defined(__cplusplus)
+}
+#endif
+
+#define issue_212_H_DEFINED
+#endif /* issue_212_H */
diff --git a/out/test-issue_96/issue_96.c b/out/test-issue_96/issue_96.c
index b992288f..09544d42 100644
--- a/out/test-issue_96/issue_96.c
+++ b/out/test-issue_96/issue_96.c
@@ -7,7 +7,7 @@
 
 #include "issue_96.h"
 
-void issue_96_use_it(issue_96_MyStruct *x)
+void issue_96_use_it(Eurydice_arr_3f *x)
 {
   EURYDICE_ASSERT(!!((size_t)0U < (size_t)5U), "assert failure");
 }
@@ -19,9 +19,9 @@ void issue_96_use_it2(issue_96_MyStruct2 *x)
 
 void issue_96_main(void)
 {
-  issue_96_MyStruct x = { .fst = { 0U } };
+  Eurydice_arr_3f x = { .data = { 0U } };
   issue_96_use_it(&x);
-  issue_96_MyStruct2 x0 = { .fst = { 0U }, .snd = 2U };
+  issue_96_MyStruct2 x0 = { .fst = { .data = { 0U } }, .snd = 2U };
   issue_96_use_it2(&x0);
 }
 
diff --git a/out/test-issue_96/issue_96.h b/out/test-issue_96/issue_96.h
index e3d59eae..71e00bae 100644
--- a/out/test-issue_96/issue_96.h
+++ b/out/test-issue_96/issue_96.h
@@ -15,16 +15,24 @@
 extern "C" {
 #endif
 
-typedef struct issue_96_MyStruct_s { uint8_t fst[5U]; } issue_96_MyStruct;
+/**
+A monomorphic instance of Eurydice.arr
+with types uint8_t
+with const generics
+- $5size_t
+*/
+typedef struct Eurydice_arr_3f_s { uint8_t data[5U]; } Eurydice_arr_3f;
+
+typedef Eurydice_arr_3f issue_96_MyStruct;
 
 typedef struct issue_96_MyStruct2_s
 {
-  uint8_t fst[5U];
+  Eurydice_arr_3f fst;
   uint32_t snd;
 }
 issue_96_MyStruct2;
 
-void issue_96_use_it(issue_96_MyStruct *x);
+void issue_96_use_it(Eurydice_arr_3f *x);
 
 void issue_96_use_it2(issue_96_MyStruct2 *x);
 
diff --git a/out/test-issue_k630/issue_k630.c b/out/test-issue_k630/issue_k630.c
index 1b4c0d05..89bf717b 100644
--- a/out/test-issue_k630/issue_k630.c
+++ b/out/test-issue_k630/issue_k630.c
@@ -16,16 +16,20 @@ _uint32_t__x2;
 
 void issue_k630_main(void)
 {
-  uint32_t v[5U][1U];
+  Eurydice_arr_10 v;
+  Eurydice_arr_a5 repeat_expression0[5U];
   KRML_MAYBE_FOR5(i,
     (size_t)0U,
     (size_t)5U,
     (size_t)1U,
+    Eurydice_arr_a5 lit;
     uint32_t repeat_expression = 2U;
-    memcpy(v[i], &repeat_expression, (size_t)1U * sizeof (uint32_t)););
+    memcpy(lit.data, &repeat_expression, (size_t)1U * sizeof (uint32_t));
+    repeat_expression0[i] = lit;);
+  memcpy(v.data, repeat_expression0, (size_t)5U * sizeof (Eurydice_arr_a5));
   /* original Rust expression is not an lvalue in C */
   uint32_t lvalue = 2U;
-  _uint32_t__x2 uu____0 = { .fst = v[0U], .snd = &lvalue };
+  _uint32_t__x2 uu____0 = { .fst = v.data->data, .snd = &lvalue };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
 }
 
diff --git a/out/test-issue_k630/issue_k630.h b/out/test-issue_k630/issue_k630.h
index ede2728a..5b4bdfd6 100644
--- a/out/test-issue_k630/issue_k630.h
+++ b/out/test-issue_k630/issue_k630.h
@@ -21,6 +21,22 @@ extern "C" {
 
 typedef uint8_t core_panicking_AssertKind;
 
+/**
+A monomorphic instance of Eurydice.arr
+with types uint32_t
+with const generics
+- $1size_t
+*/
+typedef struct Eurydice_arr_a5_s { uint32_t data[1U]; } Eurydice_arr_a5;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr uint32_t[[$1size_t]]
+with const generics
+- $5size_t
+*/
+typedef struct Eurydice_arr_10_s { Eurydice_arr_a5 data[5U]; } Eurydice_arr_10;
+
 void issue_k630_main(void);
 
 #if defined(__cplusplus)
diff --git a/out/test-more_primitive_types/more_primitive_types.c b/out/test-more_primitive_types/more_primitive_types.c
index 1fc60ca7..aa4905b9 100644
--- a/out/test-more_primitive_types/more_primitive_types.c
+++ b/out/test-more_primitive_types/more_primitive_types.c
@@ -104,9 +104,19 @@ int32_t more_primitive_types_match_i128(more_primitive_types_MorePrimitiveTypes
   return (int32_t)3;
 }
 
+/**
+A monomorphic instance of Eurydice.arr
+with types uint8_t
+with const generics
+- $6size_t
+*/
+typedef struct arr_fd_s { uint8_t data[6U]; } arr_fd;
+
 void more_primitive_types_use_more_primitive_types(void)
 {
-  uint8_t s[6U] = { 97U, 104U, 101U, 108U, 108U, 111U };
+  /* original Rust expression is not an lvalue in C */
+  arr_fd lvalue = { .data = { 97U, 104U, 101U, 108U, 108U, 111U } };
+  arr_fd *s = &lvalue;
   more_primitive_types_MorePrimitiveTypes
   p =
     {
@@ -116,7 +126,7 @@ void more_primitive_types_use_more_primitive_types(void)
     };
   more_primitive_types_match_u128(&p);
   more_primitive_types_match_i128(&p);
-  EURYDICE_ASSERT(p.c == (uint32_t)s[0U], "panic!");
+  EURYDICE_ASSERT(p.c == (uint32_t)s->data[0U], "panic!");
 }
 
 void more_primitive_types_main(void)
diff --git a/out/test-nested_arrays/nested_arrays.c b/out/test-nested_arrays/nested_arrays.c
index e063c17c..74019f68 100644
--- a/out/test-nested_arrays/nested_arrays.c
+++ b/out/test-nested_arrays/nested_arrays.c
@@ -7,8 +7,6 @@
 
 #include "nested_arrays.h"
 
-const uint32_t nested_arrays_ZERO[8U] = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U };
-
 typedef struct _uint32_t__x2_s
 {
   uint32_t *fst;
@@ -18,16 +16,20 @@ _uint32_t__x2;
 
 void nested_arrays_main(void)
 {
-  uint32_t keys[3U][3U][8U];
+  Eurydice_arr_0c keys;
+  Eurydice_arr_99 repeat_expression0[3U];
   for (size_t i0 = (size_t)0U; i0 < (size_t)3U; i0++)
   {
-    uint32_t repeat_expression[3U][8U];
+    Eurydice_arr_99 lit;
+    nested_arrays_Key repeat_expression[3U];
     for (size_t i = (size_t)0U; i < (size_t)3U; i++)
     {
-      memcpy(repeat_expression[i], nested_arrays_ZERO, (size_t)8U * sizeof (uint32_t));
+      repeat_expression[i] = NESTED_ARRAYS_ZERO;
     }
-    memcpy(keys[i0], repeat_expression, (size_t)3U * sizeof (uint32_t [8U]));
+    memcpy(lit.data, repeat_expression, (size_t)3U * sizeof (nested_arrays_Key));
+    repeat_expression0[i0] = lit;
   }
+  memcpy(keys.data, repeat_expression0, (size_t)3U * sizeof (Eurydice_arr_99));
   for (size_t i0 = (size_t)0U; i0 < (size_t)3U; i0++)
   {
     size_t i1 = i0;
@@ -37,7 +39,7 @@ void nested_arrays_main(void)
       for (size_t i = (size_t)0U; i < (size_t)8U; i++)
       {
         size_t k = i;
-        uint32_t actual = keys[i1][j][k];
+        uint32_t actual = keys.data[i1].data[j].data[k];
         uint32_t expected = (uint32_t)k;
         _uint32_t__x2 uu____0 = { .fst = &actual, .snd = &expected };
         EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
@@ -46,26 +48,12 @@ void nested_arrays_main(void)
   }
 }
 
-void nested_arrays_test(uint8_t ret[4U][200U])
+Eurydice_arr_70 nested_arrays_test(void)
 {
-  uint8_t out0[200U] = { 0U };
-  uint8_t out1[200U] = { 0U };
-  uint8_t out2[200U] = { 0U };
-  uint8_t out3[200U] = { 0U };
-  /* Passing arrays by value in Rust generates a copy in C */
-  uint8_t copy_of_out0[200U];
-  memcpy(copy_of_out0, out0, (size_t)200U * sizeof (uint8_t));
-  /* Passing arrays by value in Rust generates a copy in C */
-  uint8_t copy_of_out1[200U];
-  memcpy(copy_of_out1, out1, (size_t)200U * sizeof (uint8_t));
-  /* Passing arrays by value in Rust generates a copy in C */
-  uint8_t copy_of_out2[200U];
-  memcpy(copy_of_out2, out2, (size_t)200U * sizeof (uint8_t));
-  uint8_t uu____3[200U];
-  memcpy(uu____3, out3, (size_t)200U * sizeof (uint8_t));
-  memcpy(ret[0U], copy_of_out0, (size_t)200U * sizeof (uint8_t));
-  memcpy(ret[1U], copy_of_out1, (size_t)200U * sizeof (uint8_t));
-  memcpy(ret[2U], copy_of_out2, (size_t)200U * sizeof (uint8_t));
-  memcpy(ret[3U], uu____3, (size_t)200U * sizeof (uint8_t));
+  Eurydice_arr_88 out0 = { .data = { 0U } };
+  Eurydice_arr_88 out1 = { .data = { 0U } };
+  Eurydice_arr_88 out2 = { .data = { 0U } };
+  Eurydice_arr_88 out3 = { .data = { 0U } };
+  return (KRML_CLITERAL(Eurydice_arr_70){ .data = { out0, out1, out2, out3 } });
 }
 
diff --git a/out/test-nested_arrays/nested_arrays.h b/out/test-nested_arrays/nested_arrays.h
index c12cd3ee..e2bb3edf 100644
--- a/out/test-nested_arrays/nested_arrays.h
+++ b/out/test-nested_arrays/nested_arrays.h
@@ -84,13 +84,45 @@ core_iter_range__core__iter__range__Step_for_usize__steps_between(size_t *x0, si
 
 typedef uint8_t core_panicking_AssertKind;
 
-typedef uint32_t nested_arrays_Key[8U];
+typedef struct nested_arrays_Key_s { uint32_t data[8U]; } nested_arrays_Key;
 
-extern const uint32_t nested_arrays_ZERO[8U];
+#define NESTED_ARRAYS_ZERO ((KRML_CLITERAL(nested_arrays_Key){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U } }))
+
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr uint32_t[[$8size_t]]
+with const generics
+- $3size_t
+*/
+typedef struct Eurydice_arr_99_s { nested_arrays_Key data[3U]; } Eurydice_arr_99;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr Eurydice_arr uint32_t[[$8size_t]][[$3size_t]]
+with const generics
+- $3size_t
+*/
+typedef struct Eurydice_arr_0c_s { Eurydice_arr_99 data[3U]; } Eurydice_arr_0c;
 
 void nested_arrays_main(void);
 
-void nested_arrays_test(uint8_t ret[4U][200U]);
+/**
+A monomorphic instance of Eurydice.arr
+with types uint8_t
+with const generics
+- $200size_t
+*/
+typedef struct Eurydice_arr_88_s { uint8_t data[200U]; } Eurydice_arr_88;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr uint8_t[[$200size_t]]
+with const generics
+- $4size_t
+*/
+typedef struct Eurydice_arr_70_s { Eurydice_arr_88 data[4U]; } Eurydice_arr_70;
+
+Eurydice_arr_70 nested_arrays_test(void);
 
 #if defined(__cplusplus)
 }
diff --git a/out/test-nested_arrays2/nested_arrays2.c b/out/test-nested_arrays2/nested_arrays2.c
index 1ed4f50f..03b13f21 100644
--- a/out/test-nested_arrays2/nested_arrays2.c
+++ b/out/test-nested_arrays2/nested_arrays2.c
@@ -7,8 +7,6 @@
 
 #include "nested_arrays2.h"
 
-const uint8_t nested_arrays2_TABLE[1U][1U] = { { 1U } };
-
 void nested_arrays2_main(void)
 {
 
diff --git a/out/test-nested_arrays2/nested_arrays2.h b/out/test-nested_arrays2/nested_arrays2.h
index d14ce144..49ee8164 100644
--- a/out/test-nested_arrays2/nested_arrays2.h
+++ b/out/test-nested_arrays2/nested_arrays2.h
@@ -15,7 +15,23 @@
 extern "C" {
 #endif
 
-extern const uint8_t nested_arrays2_TABLE[1U][1U];
+/**
+A monomorphic instance of Eurydice.arr
+with types uint8_t
+with const generics
+- $1size_t
+*/
+typedef struct Eurydice_arr_f1_s { uint8_t data[1U]; } Eurydice_arr_f1;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr uint8_t[[$1size_t]]
+with const generics
+- $1size_t
+*/
+typedef struct Eurydice_arr_81_s { Eurydice_arr_f1 data[1U]; } Eurydice_arr_81;
+
+#define NESTED_ARRAYS2_TABLE ((KRML_CLITERAL(Eurydice_arr_81){ .data = { (KRML_CLITERAL(Eurydice_arr_f1){ .data = { 1U } }) } }))
 
 void nested_arrays2_main(void);
 
diff --git a/out/test-repeat/repeat.c b/out/test-repeat/repeat.c
index dfdad88c..14d7e0e9 100644
--- a/out/test-repeat/repeat.c
+++ b/out/test-repeat/repeat.c
@@ -7,282 +7,12 @@
 
 #include "repeat.h"
 
-const uint32_t repeat_C1[1U] = { 0U };
-
-const uint32_t repeat_C2[1U][1U] = { { 0U } };
-
-const
-uint8_t
-repeat_REJECTION_SAMPLE_SHUFFLE_TABLE[256U][16U] =
-  {
-    {
-      255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U
-    },
-    { 0U, 1U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U },
-    {
-      10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U
-    }, { 0U, 1U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U },
-    {
-      12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U
-    }, { 0U, 1U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U },
-    { 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U },
-    { 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U },
-    {
-      14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U
-    }, { 0U, 1U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U },
-    { 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U },
-    { 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U },
-    { 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U },
-    { 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U },
-    { 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U },
-    { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U },
-    { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U },
-    { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U }
-  };
-
 void repeat_main(void)
 {
   if
   (
-    !(repeat_C1[0U] + repeat_C2[0U][0U] + (uint32_t)repeat_REJECTION_SAMPLE_SHUFFLE_TABLE[255U][0U]
+    !(REPEAT_C1.data[0U] + REPEAT_C2.data->data[0U] +
+      (uint32_t)REPEAT_REJECTION_SAMPLE_SHUFFLE_TABLE.data[255U].data[0U]
     != 0U)
   )
   {
diff --git a/out/test-repeat/repeat.h b/out/test-repeat/repeat.h
index 99d3262b..4101741c 100644
--- a/out/test-repeat/repeat.h
+++ b/out/test-repeat/repeat.h
@@ -15,11 +15,43 @@
 extern "C" {
 #endif
 
-extern const uint32_t repeat_C1[1U];
-
-extern const uint32_t repeat_C2[1U][1U];
-
-extern const uint8_t repeat_REJECTION_SAMPLE_SHUFFLE_TABLE[256U][16U];
+/**
+A monomorphic instance of Eurydice.arr
+with types uint32_t
+with const generics
+- $1size_t
+*/
+typedef struct Eurydice_arr_a5_s { uint32_t data[1U]; } Eurydice_arr_a5;
+
+#define REPEAT_C1 ((KRML_CLITERAL(Eurydice_arr_a5){ .data = { 0U } }))
+
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr uint32_t[[$1size_t]]
+with const generics
+- $1size_t
+*/
+typedef struct Eurydice_arr_81_s { Eurydice_arr_a5 data[1U]; } Eurydice_arr_81;
+
+#define REPEAT_C2 ((KRML_CLITERAL(Eurydice_arr_81){ .data = { (KRML_CLITERAL(Eurydice_arr_a5){ .data = { 0U } }) } }))
+
+/**
+A monomorphic instance of Eurydice.arr
+with types uint8_t
+with const generics
+- $16size_t
+*/
+typedef struct Eurydice_arr_88_s { uint8_t data[16U]; } Eurydice_arr_88;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr uint8_t[[$16size_t]]
+with const generics
+- $256size_t
+*/
+typedef struct Eurydice_arr_ef_s { Eurydice_arr_88 data[256U]; } Eurydice_arr_ef;
+
+#define REPEAT_REJECTION_SAMPLE_SHUFFLE_TABLE ((KRML_CLITERAL(Eurydice_arr_ef){ .data = { (KRML_CLITERAL(Eurydice_arr_88){ .data = { 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 14U, 15U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 12U, 13U, 14U, 15U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U, 255U, 255U } }), (KRML_CLITERAL(Eurydice_arr_88){ .data = { 0U, 1U, 2U, 3U, 4U, 5U, 6U, 7U, 8U, 9U, 10U, 11U, 12U, 13U, 14U, 15U } }) } }))
 
 void repeat_main(void);
 
diff --git a/out/test-slice_array/slice_array.c b/out/test-slice_array/slice_array.c
index 65437f62..281b70c7 100644
--- a/out/test-slice_array/slice_array.c
+++ b/out/test-slice_array/slice_array.c
@@ -16,15 +16,24 @@ _uint8_t__x2;
 
 void slice_array_f1(void)
 {
-  uint8_t x[4U][4U] = { { 0U } };
+  Eurydice_arr_11
+  x =
+    {
+      .data = {
+        (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+        (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+        (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+        (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } })
+      }
+    };
   Eurydice_slice
   y0 =
-    Eurydice_slice_split_at_mut(Eurydice_array_to_slice((size_t)4U, x, uint8_t [4U]),
+    Eurydice_slice_split_at_mut(Eurydice_array_to_slice((size_t)4U, &x, Eurydice_arr_e9),
       (size_t)2U,
-      uint8_t [4U],
-      Eurydice_slice_uint8_t_4size_t__x2).fst;
-  Eurydice_slice_index(y0, (size_t)0U, uint8_t [4U], uint8_t (*)[4U])[0U] = 1U;
-  uint8_t actual = x[0U][0U];
+      Eurydice_arr_e9,
+      Eurydice_slice_Eurydice_arr_uint8_t___4size_t___x2).fst;
+  Eurydice_slice_index(y0, (size_t)0U, Eurydice_arr_e9, Eurydice_arr_e9 *).data[0U] = 1U;
+  uint8_t actual = x.data->data[0U];
   uint8_t expected = 1U;
   _uint8_t__x2 uu____0 = { .fst = &actual, .snd = &expected };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
@@ -32,22 +41,32 @@ void slice_array_f1(void)
 
 void slice_array_f2(void)
 {
-  uint8_t x[4U][4U] = { { 0U } };
+  Eurydice_arr_11
+  x =
+    {
+      .data = {
+        (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+        (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+        (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+        (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } })
+      }
+    };
   Eurydice_slice
   y0 =
-    Eurydice_slice_split_at_mut(Eurydice_array_to_slice((size_t)4U, x, uint8_t [4U]),
+    Eurydice_slice_split_at_mut(Eurydice_array_to_slice((size_t)4U, &x, Eurydice_arr_e9),
       (size_t)2U,
-      uint8_t [4U],
-      Eurydice_slice_uint8_t_4size_t__x2).fst;
-  uint8_t z[4U];
-  memcpy(z,
-    Eurydice_slice_index(y0, (size_t)0U, uint8_t [4U], uint8_t (*)[4U]),
-    (size_t)4U * sizeof (uint8_t));
-  z[0U] = 1U;
-  uint8_t actual = x[0U][0U];
+      Eurydice_arr_e9,
+      Eurydice_slice_Eurydice_arr_uint8_t___4size_t___x2).fst;
+  Eurydice_arr_e9 z = Eurydice_slice_index(y0, (size_t)0U, Eurydice_arr_e9, Eurydice_arr_e9 *);
+  z.data[0U] = 1U;
+  uint8_t actual = x.data->data[0U];
   uint8_t expected = 0U;
   _uint8_t__x2 uu____0 = { .fst = &actual, .snd = &expected };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
+  /* original Rust expression is not an lvalue in C */
+  uint8_t lvalue = 1U;
+  _uint8_t__x2 uu____1 = { .fst = z.data, .snd = &lvalue };
+  EURYDICE_ASSERT(uu____1.fst[0U] == uu____1.snd[0U], "panic!");
 }
 
 void slice_array_main(void)
diff --git a/out/test-slice_array/slice_array.h b/out/test-slice_array/slice_array.h
index 38667573..0266e487 100644
--- a/out/test-slice_array/slice_array.h
+++ b/out/test-slice_array/slice_array.h
@@ -21,12 +21,20 @@ extern "C" {
 
 typedef uint8_t core_panicking_AssertKind;
 
-typedef struct Eurydice_slice_uint8_t_4size_t__x2_s
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr uint8_t[[$4size_t]]
+with const generics
+- $4size_t
+*/
+typedef struct Eurydice_arr_11_s { Eurydice_arr_e9 data[4U]; } Eurydice_arr_11;
+
+typedef struct Eurydice_slice_Eurydice_arr_uint8_t___4size_t___x2_s
 {
   Eurydice_slice fst;
   Eurydice_slice snd;
 }
-Eurydice_slice_uint8_t_4size_t__x2;
+Eurydice_slice_Eurydice_arr_uint8_t___4size_t___x2;
 
 void slice_array_f1(void);
 
diff --git a/out/test-symcrust/symcrust.c b/out/test-symcrust/symcrust.c
index de981de6..df73cdff 100644
--- a/out/test-symcrust/symcrust.c
+++ b/out/test-symcrust/symcrust.c
@@ -12,7 +12,7 @@
 
 void
 symcrust_SymCrustMlKemPolyElementCompressAndEncode(
-  uint16_t *coeffs,
+  Eurydice_arr_bc *coeffs,
   uint32_t nBitsPerCoefficient,
   Eurydice_slice dst
 )
@@ -31,7 +31,7 @@ symcrust_SymCrustMlKemPolyElementCompressAndEncode(
   {
     size_t i0 = i;
     uint32_t nBitsInCoefficient = nBitsPerCoefficient;
-    uint32_t coefficient = (uint32_t)coeffs[i0];
+    uint32_t coefficient = (uint32_t)coeffs->data[i0];
     if (nBitsPerCoefficient < 12U)
     {
       uint64_t multiplication = (uint64_t)coefficient * SYMCRYPT_MLKEM_COMPRESS_MULCONSTANT;
@@ -54,9 +54,11 @@ symcrust_SymCrustMlKemPolyElementCompressAndEncode(
       {
         Eurydice_slice
         uu____0 = Eurydice_slice_subslice3(dst, cbDstWritten, cbDstWritten + (size_t)4U, uint8_t *);
-        uint8_t ret[4U];
-        core_num__u32__to_le_bytes(accumulator, ret);
-        Eurydice_slice_copy(uu____0, Eurydice_array_to_slice((size_t)4U, ret, uint8_t), uint8_t);
+        /* original Rust expression is not an lvalue in C */
+        Eurydice_arr_e9 lvalue = core_num__u32__to_le_bytes(accumulator);
+        Eurydice_slice_copy(uu____0,
+          Eurydice_array_to_slice((size_t)4U, &lvalue, uint8_t),
+          uint8_t);
         cbDstWritten = cbDstWritten + (size_t)4U;
         accumulator = 0U;
         nBitsInAccumulator = 0U;
diff --git a/out/test-symcrust/symcrust.h b/out/test-symcrust/symcrust.h
index 0f294c08..9a0bca27 100644
--- a/out/test-symcrust/symcrust.h
+++ b/out/test-symcrust/symcrust.h
@@ -96,11 +96,19 @@ tuple_04;
 extern tuple_04
 core_iter_range__core__iter__range__Step_for_usize__steps_between(size_t *x0, size_t *x1);
 
-static inline void core_num__u32__to_le_bytes(uint32_t x0, uint8_t x1[4U]);
+static inline Eurydice_arr_e9 core_num__u32__to_le_bytes(uint32_t x0);
+
+/**
+A monomorphic instance of Eurydice.arr
+with types uint16_t
+with const generics
+- $256size_t
+*/
+typedef struct Eurydice_arr_bc_s { uint16_t data[256U]; } Eurydice_arr_bc;
 
 void
 symcrust_SymCrustMlKemPolyElementCompressAndEncode(
-  uint16_t *coeffs,
+  Eurydice_arr_bc *coeffs,
   uint32_t nBitsPerCoefficient,
   Eurydice_slice dst
 );
diff --git a/out/test-traits/traits.c b/out/test-traits/traits.c
index cd8b6315..115d887d 100644
--- a/out/test-traits/traits.c
+++ b/out/test-traits/traits.c
@@ -48,10 +48,10 @@ uint32_t traits_to_int_88(Eurydice_slice *self)
 
 void traits_main(void)
 {
-  traits_Foo foos[2U] = { traits_Foo_Foo1, traits_Foo_Foo2 };
+  Eurydice_arr_e2 foos = { .data = { traits_Foo_Foo1, traits_Foo_Foo2 } };
   /* original Rust expression is not an lvalue in C */
   Eurydice_slice
-  lvalue = Eurydice_array_to_subslice3(foos, (size_t)0U, (size_t)2U, traits_Foo *);
+  lvalue = Eurydice_array_to_subslice3(&foos, (size_t)0U, (size_t)2U, traits_Foo *);
   if (!(traits_to_int_88(&lvalue) != 2U))
   {
     return;
diff --git a/out/test-traits/traits.h b/out/test-traits/traits.h
index 7bba5518..1bea79d7 100644
--- a/out/test-traits/traits.h
+++ b/out/test-traits/traits.h
@@ -32,6 +32,14 @@ This function found in impl {traits::ToInt for &0 (@Slice<traits::Foo>)}
 */
 uint32_t traits_to_int_88(Eurydice_slice *self);
 
+/**
+A monomorphic instance of Eurydice.arr
+with types traits_Foo
+with const generics
+- $2size_t
+*/
+typedef struct Eurydice_arr_e2_s { traits_Foo data[2U]; } Eurydice_arr_e2;
+
 void traits_main(void);
 
 #if defined(__cplusplus)
diff --git a/out/test-where_clauses_closures/where_clauses_closures.c b/out/test-where_clauses_closures/where_clauses_closures.c
index c028b5e0..08a58997 100644
--- a/out/test-where_clauses_closures/where_clauses_closures.c
+++ b/out/test-where_clauses_closures/where_clauses_closures.c
@@ -62,14 +62,15 @@ with const generics
 */
 size_t_x2 where_clauses_closures_test_e3(void)
 {
-  size_t x[1U];
+  Eurydice_arr_e4 arr_struct;
   {
     /* original Rust expression is not an lvalue in C */
     void *lvalue = (void *)0U;
-    x[0U] = where_clauses_closures_test_call_mut_1a_e3(&lvalue, (size_t)0U);
+    arr_struct.data[0U] = where_clauses_closures_test_call_mut_1a_e3(&lvalue, (size_t)0U);
   }
+  Eurydice_arr_e4 x = arr_struct;
   size_t y = where_clauses_closures_zero_38();
-  return (KRML_CLITERAL(size_t_x2){ .fst = x[0U], .snd = y });
+  return (KRML_CLITERAL(size_t_x2){ .fst = x.data[0U], .snd = y });
 }
 
 typedef struct _size_t__x2_s
diff --git a/out/test-where_clauses_closures/where_clauses_closures.h b/out/test-where_clauses_closures/where_clauses_closures.h
index e698334e..6763485f 100644
--- a/out/test-where_clauses_closures/where_clauses_closures.h
+++ b/out/test-where_clauses_closures/where_clauses_closures.h
@@ -62,6 +62,14 @@ typedef struct size_t_x2_s
 }
 size_t_x2;
 
+/**
+A monomorphic instance of Eurydice.arr
+with types size_t
+with const generics
+- $1size_t
+*/
+typedef struct Eurydice_arr_e4_s { size_t data[1U]; } Eurydice_arr_e4;
+
 /**
 A monomorphic instance of where_clauses_closures.test
 with types size_t
diff --git a/out/test-where_clauses_fncg/where_clauses_fncg.c b/out/test-where_clauses_fncg/where_clauses_fncg.c
index 1b5db4ee..8a45995d 100644
--- a/out/test-where_clauses_fncg/where_clauses_fncg.c
+++ b/out/test-where_clauses_fncg/where_clauses_fncg.c
@@ -16,9 +16,9 @@ with const generics
 - K= 8
 - L= 4
 */
-uint64_t where_clauses_fncg_bar_16_7b(uint8_t x[8U][4U], uint8_t _[4U][8U])
+uint64_t where_clauses_fncg_bar_16_7b(Eurydice_arr_cb x, Eurydice_arr_1c _)
 {
-  return (uint64_t)x[0U][0U];
+  return (uint64_t)x.data->data[0U];
 }
 
 /**
@@ -31,9 +31,31 @@ with const generics
 */
 uint64_t where_clauses_fncg_f_43(void)
 {
-  uint8_t buf0[8U][4U] = { { 0U } };
-  uint8_t buf[4U][8U] = { { 0U } };
-  return where_clauses_fncg_bar_16_7b(buf0, buf);
+  return
+    where_clauses_fncg_bar_16_7b((
+        KRML_CLITERAL(Eurydice_arr_cb){
+          .data = {
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } })
+          }
+        }
+      ),
+      (
+        KRML_CLITERAL(Eurydice_arr_1c){
+          .data = {
+            (KRML_CLITERAL(Eurydice_arr_c4){ .data = { 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_c4){ .data = { 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_c4){ .data = { 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_c4){ .data = { 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U } })
+          }
+        }
+      ));
 }
 
 /**
@@ -45,9 +67,9 @@ with const generics
 - K= 12
 - L= 4
 */
-uint64_t where_clauses_fncg_bar_16_fa(uint8_t x[12U][4U], uint8_t _[4U][12U])
+uint64_t where_clauses_fncg_bar_16_fa(Eurydice_arr_91 x, Eurydice_arr_b1 _)
 {
-  return (uint64_t)x[0U][0U];
+  return (uint64_t)x.data->data[0U];
 }
 
 /**
@@ -61,9 +83,51 @@ with const generics
 */
 uint64_t where_clauses_fncg_method_foo_db_7c(void)
 {
-  uint8_t buf0[12U][4U] = { { 0U } };
-  uint8_t buf[4U][12U] = { { 0U } };
-  return where_clauses_fncg_bar_16_fa(buf0, buf);
+  return
+    where_clauses_fncg_bar_16_fa((
+        KRML_CLITERAL(Eurydice_arr_91){
+          .data = {
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } }),
+            (KRML_CLITERAL(Eurydice_arr_e9){ .data = { 0U, 0U, 0U, 0U } })
+          }
+        }
+      ),
+      (
+        KRML_CLITERAL(Eurydice_arr_b1){
+          .data = {
+            (
+              KRML_CLITERAL(Eurydice_arr_48){
+                .data = { 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U }
+              }
+            ),
+            (
+              KRML_CLITERAL(Eurydice_arr_48){
+                .data = { 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U }
+              }
+            ),
+            (
+              KRML_CLITERAL(Eurydice_arr_48){
+                .data = { 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U }
+              }
+            ),
+            (
+              KRML_CLITERAL(Eurydice_arr_48){
+                .data = { 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U, 0U }
+              }
+            )
+          }
+        }
+      ));
 }
 
 /**
diff --git a/out/test-where_clauses_fncg/where_clauses_fncg.h b/out/test-where_clauses_fncg/where_clauses_fncg.h
index 2f05d05a..584231b3 100644
--- a/out/test-where_clauses_fncg/where_clauses_fncg.h
+++ b/out/test-where_clauses_fncg/where_clauses_fncg.h
@@ -23,6 +23,22 @@ static inline uint64_t core_convert_num__core__convert__From_u8__for_u64__from(u
 
 typedef uint8_t core_panicking_AssertKind;
 
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr uint8_t[[$4size_t]]
+with const generics
+- $8size_t
+*/
+typedef struct Eurydice_arr_cb_s { Eurydice_arr_e9 data[8U]; } Eurydice_arr_cb;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr uint8_t[[$8size_t]]
+with const generics
+- $4size_t
+*/
+typedef struct Eurydice_arr_1c_s { Eurydice_arr_c4 data[4U]; } Eurydice_arr_1c;
+
 /**
 This function found in impl {where_clauses_fncg::Foo<K> for u64}
 */
@@ -32,7 +48,7 @@ with const generics
 - K= 8
 - L= 4
 */
-uint64_t where_clauses_fncg_bar_16_7b(uint8_t x[8U][4U], uint8_t _[4U][8U]);
+uint64_t where_clauses_fncg_bar_16_7b(Eurydice_arr_cb x, Eurydice_arr_1c _);
 
 /**
 A monomorphic instance of where_clauses_fncg.f
@@ -44,6 +60,30 @@ with const generics
 */
 uint64_t where_clauses_fncg_f_43(void);
 
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr uint8_t[[$4size_t]]
+with const generics
+- $12size_t
+*/
+typedef struct Eurydice_arr_91_s { Eurydice_arr_e9 data[12U]; } Eurydice_arr_91;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types uint8_t
+with const generics
+- $12size_t
+*/
+typedef struct Eurydice_arr_48_s { uint8_t data[12U]; } Eurydice_arr_48;
+
+/**
+A monomorphic instance of Eurydice.arr
+with types Eurydice_arr uint8_t[[$12size_t]]
+with const generics
+- $4size_t
+*/
+typedef struct Eurydice_arr_b1_s { Eurydice_arr_48 data[4U]; } Eurydice_arr_b1;
+
 /**
 This function found in impl {where_clauses_fncg::Foo<K> for u64}
 */
@@ -53,7 +93,7 @@ with const generics
 - K= 12
 - L= 4
 */
-uint64_t where_clauses_fncg_bar_16_fa(uint8_t x[12U][4U], uint8_t _[4U][12U]);
+uint64_t where_clauses_fncg_bar_16_fa(Eurydice_arr_91 x, Eurydice_arr_b1 _);
 
 /**
 This function found in impl {where_clauses_fncg::UseFoo for ()}
diff --git a/out/test-where_clauses_simple/where_clauses_simple.c b/out/test-where_clauses_simple/where_clauses_simple.c
index a1cf9193..b3363b62 100644
--- a/out/test-where_clauses_simple/where_clauses_simple.c
+++ b/out/test-where_clauses_simple/where_clauses_simple.c
@@ -28,9 +28,9 @@ A monomorphic instance of where_clauses_simple.add_81
 with const generics
 - K= 3
 */
-size_t where_clauses_simple_add_81_e0(uint16_t x[3U], size_t y)
+size_t where_clauses_simple_add_81_e0(Eurydice_arr_7f x, size_t y)
 {
-  return (size_t)x[0U] + y + (size_t)3U;
+  return (size_t)x.data[0U] + y + (size_t)3U;
 }
 
 /**
@@ -42,8 +42,9 @@ with const generics
 size_t where_clauses_simple_fn_k_71(void)
 {
   size_t x = where_clauses_simple_of_u16_81_e0(0U);
-  uint16_t buf[3U] = { 0U };
-  return where_clauses_simple_add_81_e0(buf, x);
+  return
+    where_clauses_simple_add_81_e0((KRML_CLITERAL(Eurydice_arr_7f){ .data = { 0U, 0U, 0U } }),
+      x);
 }
 
 typedef struct _size_t__x2_s
@@ -64,9 +65,9 @@ void where_clauses_simple_k_calls_k(void)
 /**
 This function found in impl {where_clauses_simple::Ops<1usize> for u64}
 */
-uint64_t where_clauses_simple_add_19(uint16_t x[1U], uint64_t y)
+uint64_t where_clauses_simple_add_19(Eurydice_arr_2e x, uint64_t y)
 {
-  return (uint64_t)x[0U] + y;
+  return (uint64_t)x.data[0U] + y;
 }
 
 /**
@@ -83,11 +84,10 @@ with types uint64_t
 with const generics
 - K= 1
 */
-uint64_t where_clauses_simple_fn_k_3a(void)
+uint64_t where_clauses_simple_fn_k_e4(void)
 {
   uint64_t x = where_clauses_simple_of_u16_19(0U);
-  uint16_t buf[1U] = { 0U };
-  return where_clauses_simple_add_19(buf, x);
+  return where_clauses_simple_add_19((KRML_CLITERAL(Eurydice_arr_2e){ .data = { 0U } }), x);
 }
 
 typedef struct _uint64_t__x2_s
@@ -99,7 +99,7 @@ _uint64_t__x2;
 
 void where_clauses_simple_k_calls_one(void)
 {
-  uint64_t r = where_clauses_simple_fn_k_3a();
+  uint64_t r = where_clauses_simple_fn_k_e4();
   uint64_t r_expected = 0ULL;
   _uint64_t__x2 uu____0 = { .fst = &r, .snd = &r_expected };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
@@ -126,9 +126,9 @@ A monomorphic instance of where_clauses_simple.add_81
 with const generics
 - K= 1
 */
-size_t where_clauses_simple_add_81_74(uint16_t x[1U], size_t y)
+size_t where_clauses_simple_add_81_74(Eurydice_arr_2e x, size_t y)
 {
-  return (size_t)x[0U] + y + (size_t)1U;
+  return (size_t)x.data[0U] + y + (size_t)1U;
 }
 
 /**
@@ -137,16 +137,15 @@ with types size_t
 with const generics
 
 */
-size_t where_clauses_simple_fn_1_e6(void)
+size_t where_clauses_simple_fn_1_a5(void)
 {
   size_t x = where_clauses_simple_of_u16_81_74(0U);
-  uint16_t buf[1U] = { 0U };
-  return where_clauses_simple_add_81_74(buf, x);
+  return where_clauses_simple_add_81_74((KRML_CLITERAL(Eurydice_arr_2e){ .data = { 0U } }), x);
 }
 
 void where_clauses_simple_one_calls_k(void)
 {
-  size_t r = where_clauses_simple_fn_1_e6();
+  size_t r = where_clauses_simple_fn_1_a5();
   size_t r_expected = (size_t)1U;
   _size_t__x2 uu____0 = { .fst = &r, .snd = &r_expected };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
@@ -158,16 +157,15 @@ with types uint64_t
 with const generics
 
 */
-uint64_t where_clauses_simple_fn_1_d7(void)
+uint64_t where_clauses_simple_fn_1_e5(void)
 {
   uint64_t x = where_clauses_simple_of_u16_19(0U);
-  uint16_t buf[1U] = { 0U };
-  return where_clauses_simple_add_19(buf, x);
+  return where_clauses_simple_add_19((KRML_CLITERAL(Eurydice_arr_2e){ .data = { 0U } }), x);
 }
 
 void where_clauses_simple_one_calls_one(void)
 {
-  uint64_t r = where_clauses_simple_fn_1_d7();
+  uint64_t r = where_clauses_simple_fn_1_e5();
   uint64_t r_expected = 0ULL;
   _uint64_t__x2 uu____0 = { .fst = &r, .snd = &r_expected };
   EURYDICE_ASSERT(uu____0.fst[0U] == uu____0.snd[0U], "panic!");
@@ -179,13 +177,17 @@ with types uint64_t, size_t
 with const generics
 
 */
-tuple_65 where_clauses_simple_double_ed(uint64_t x, size_t y)
+tuple_65 where_clauses_simple_double_f1(uint64_t x, size_t y)
 {
-  uint16_t buf0[1U] = { 0U };
-  uint64_t uu____0 = where_clauses_simple_add_19(buf0, x);
-  uint16_t buf[1U] = { 0U };
+  uint64_t
+  uu____0 = where_clauses_simple_add_19((KRML_CLITERAL(Eurydice_arr_2e){ .data = { 0U } }), x);
   return
-    (KRML_CLITERAL(tuple_65){ .fst = uu____0, .snd = where_clauses_simple_add_81_74(buf, y) });
+    (
+      KRML_CLITERAL(tuple_65){
+        .fst = uu____0,
+        .snd = where_clauses_simple_add_81_74((KRML_CLITERAL(Eurydice_arr_2e){ .data = { 0U } }), y)
+      }
+    );
 }
 
 /**
@@ -196,10 +198,17 @@ with const generics
 */
 tuple_b6 where_clauses_simple_double_k_7b(size_t x, uint64_t y)
 {
-  uint16_t buf0[3U] = { 0U };
-  size_t uu____0 = where_clauses_simple_add_81_e0(buf0, x);
-  uint16_t buf[1U] = { 0U };
-  return (KRML_CLITERAL(tuple_b6){ .fst = uu____0, .snd = where_clauses_simple_add_19(buf, y) });
+  size_t
+  uu____0 =
+    where_clauses_simple_add_81_e0((KRML_CLITERAL(Eurydice_arr_7f){ .data = { 0U, 0U, 0U } }),
+      x);
+  return
+    (
+      KRML_CLITERAL(tuple_b6){
+        .fst = uu____0,
+        .snd = where_clauses_simple_add_19((KRML_CLITERAL(Eurydice_arr_2e){ .data = { 0U } }), y)
+      }
+    );
 }
 
 void where_clauses_simple_main(void)
@@ -208,7 +217,7 @@ void where_clauses_simple_main(void)
   where_clauses_simple_k_calls_one();
   where_clauses_simple_one_calls_k();
   where_clauses_simple_one_calls_one();
-  tuple_65 x = where_clauses_simple_double_ed(1ULL, (size_t)1U);
+  tuple_65 x = where_clauses_simple_double_f1(1ULL, (size_t)1U);
   tuple_b6 y = where_clauses_simple_double_k_7b((size_t)1U, 1ULL);
   uint64_t x_0 = 1ULL;
   size_t x_1 = (size_t)2U;
diff --git a/out/test-where_clauses_simple/where_clauses_simple.h b/out/test-where_clauses_simple/where_clauses_simple.h
index b0cfdff5..f98de829 100644
--- a/out/test-where_clauses_simple/where_clauses_simple.h
+++ b/out/test-where_clauses_simple/where_clauses_simple.h
@@ -39,6 +39,14 @@ with const generics
 */
 size_t where_clauses_simple_of_u16_81_e0(uint16_t x);
 
+/**
+A monomorphic instance of Eurydice.arr
+with types uint16_t
+with const generics
+- $3size_t
+*/
+typedef struct Eurydice_arr_7f_s { uint16_t data[3U]; } Eurydice_arr_7f;
+
 /**
 This function found in impl {where_clauses_simple::Ops<K> for usize}
 */
@@ -47,7 +55,7 @@ A monomorphic instance of where_clauses_simple.add_81
 with const generics
 - K= 3
 */
-size_t where_clauses_simple_add_81_e0(uint16_t x[3U], size_t y);
+size_t where_clauses_simple_add_81_e0(Eurydice_arr_7f x, size_t y);
 
 /**
 A monomorphic instance of where_clauses_simple.fn_k
@@ -59,10 +67,18 @@ size_t where_clauses_simple_fn_k_71(void);
 
 void where_clauses_simple_k_calls_k(void);
 
+/**
+A monomorphic instance of Eurydice.arr
+with types uint16_t
+with const generics
+- $1size_t
+*/
+typedef struct Eurydice_arr_2e_s { uint16_t data[1U]; } Eurydice_arr_2e;
+
 /**
 This function found in impl {where_clauses_simple::Ops<1usize> for u64}
 */
-uint64_t where_clauses_simple_add_19(uint16_t x[1U], uint64_t y);
+uint64_t where_clauses_simple_add_19(Eurydice_arr_2e x, uint64_t y);
 
 /**
 This function found in impl {where_clauses_simple::Ops<1usize> for u64}
@@ -75,7 +91,7 @@ with types uint64_t
 with const generics
 - K= 1
 */
-uint64_t where_clauses_simple_fn_k_3a(void);
+uint64_t where_clauses_simple_fn_k_e4(void);
 
 void where_clauses_simple_k_calls_one(void);
 
@@ -97,7 +113,7 @@ A monomorphic instance of where_clauses_simple.add_81
 with const generics
 - K= 1
 */
-size_t where_clauses_simple_add_81_74(uint16_t x[1U], size_t y);
+size_t where_clauses_simple_add_81_74(Eurydice_arr_2e x, size_t y);
 
 /**
 A monomorphic instance of where_clauses_simple.fn_1
@@ -105,7 +121,7 @@ with types size_t
 with const generics
 
 */
-size_t where_clauses_simple_fn_1_e6(void);
+size_t where_clauses_simple_fn_1_a5(void);
 
 void where_clauses_simple_one_calls_k(void);
 
@@ -115,7 +131,7 @@ with types uint64_t
 with const generics
 
 */
-uint64_t where_clauses_simple_fn_1_d7(void);
+uint64_t where_clauses_simple_fn_1_e5(void);
 
 void where_clauses_simple_one_calls_one(void);
 
@@ -137,7 +153,7 @@ with types uint64_t, size_t
 with const generics
 
 */
-tuple_65 where_clauses_simple_double_ed(uint64_t x, size_t y);
+tuple_65 where_clauses_simple_double_f1(uint64_t x, size_t y);
 
 /**
 A monomorphic instance of K.
diff --git a/test/array.rs b/test/array.rs
index b57e22c2..aafd0470 100644
--- a/test/array.rs
+++ b/test/array.rs
@@ -11,6 +11,7 @@ fn mut_foo(mut f: Foo) {
     f.x[0] = 1u32;
     let mut copy: [u32; 2] = f.y;
     copy[0] = 0u32;
+    assert!(copy[0]!=1u32);
 }
 
 fn mk_foo() -> Foo {
@@ -40,6 +41,10 @@ fn plus_one<const K: usize>(x: [u32; K]) -> [u16; K] {
     x.map(|x| (x + 1) as u16)
 }
 
+fn const_eq<const K:usize>(x: [u32; K], y: [u32; K]) -> bool {
+   x == y
+}
+
 fn main() {
     // XXX1
     let Foo { x, y } = mk_foo2();
@@ -64,4 +69,10 @@ fn main() {
     // XXX5
     let a = nested_from_fn::<4>();
     assert_eq!(a[3][3], 6);
+
+    // XXX6
+    let x = [2u32; 2];
+    let y = [2u32; 2];
+    let b = const_eq(x,y);
+    assert_eq!(b, true);
 }
diff --git a/test/castunsize.rs b/test/castunsize.rs
new file mode 100644
index 00000000..6d84dc2e
--- /dev/null
+++ b/test/castunsize.rs
@@ -0,0 +1,35 @@
+struct S<U: ?Sized> {
+    foo: u32,
+    my_data: U,
+}
+
+type T = S<[u32]>;
+
+fn main1() {
+    let x = S { foo: 0, my_data: [0 ; 4] };
+    let x: &T = &x;
+    assert_eq!(x.my_data[3],0);
+}
+
+fn main2<const K:usize>() {
+    let x = S { foo: 0, my_data: [0 ; K] };
+    let x: &T = &x;
+    assert_eq!(x.my_data[3],0);
+}
+
+fn main3() {
+    let x: Box<[u32]> = Box::new([0; 4]);
+    assert_eq!(x[3], 0);
+}
+
+fn main4<const K:usize>() {
+    let x: Box<[u32]> = Box::new([0; K]);
+    assert_eq!(x[3], 0);
+}
+
+fn main() {
+    main1();
+    main2::<5>();
+    main3();
+    main4::<5>();
+}
diff --git a/test/issue_212.rs b/test/issue_212.rs
new file mode 100644
index 00000000..4440b200
--- /dev/null
+++ b/test/issue_212.rs
@@ -0,0 +1,7 @@
+fn id_mut<'a, T>(x : &'a T) -> &'a T { x }
+
+fn main() {
+  let arr : [i32; 3] = [1,2,3];
+  let r : &[i32; 3] = id_mut(&arr);
+  assert!(r[0] > 0);
+}
diff --git a/test/slice_array.rs b/test/slice_array.rs
index cb7daa92..4bc8bd9a 100644
--- a/test/slice_array.rs
+++ b/test/slice_array.rs
@@ -16,6 +16,7 @@ fn f2() {
     let actual = x[0][0];
     let expected = 0;
     assert_eq!(actual, expected);
+    assert_eq!(z[0],1);
 }
 
 fn main() {