+ redef fun copy_to(start, len, dest, new_start)
+ do
+ # Fast code when source and destination are two arrays
+
+ if not dest isa Array[E] then
+ super
+ return
+ end
+
+ # Enlarge dest if required
+ var dest_len = new_start + len
+ if dest_len > dest.length then
+ dest.enlarge(dest_len)
+ dest.length = dest_len
+ end
+
+ # Get underlying native arrays
+ var items = self.items
+ if items == null then return
+ var dest_items = dest.items
+ assert dest_items != null
+
+ # Native copy
+ items.memmove(start, len, dest_items, new_start)
+ end
+