aboutsummaryrefslogtreecommitdiff
path: root/discocaml/arraylist.ml
diff options
context:
space:
mode:
authorNathan Ringo <nathan@remexre.com>2024-01-19 19:37:08 -0600
committerNathan Ringo <nathan@remexre.com>2024-01-19 19:37:08 -0600
commita84e462b596c24d2562d766ceb019761085390c5 (patch)
tree51a87e24426a5ad9d94bab104e21d3d3ecbbb9f1 /discocaml/arraylist.ml
parent401bc1c5485e26329598d59a140e51f70f58857c (diff)
Use GADTs for prims, actual redex finding.
Diffstat (limited to 'discocaml/arraylist.ml')
-rw-r--r--discocaml/arraylist.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/discocaml/arraylist.ml b/discocaml/arraylist.ml
index d1a9ecd..110cd17 100644
--- a/discocaml/arraylist.ml
+++ b/discocaml/arraylist.ml
@@ -28,6 +28,7 @@ let%test _ = next_pow2 12345 = 16384
let make len dummy =
{ array = Array.make (max (next_pow2 len) 4) dummy; dummy; len }
+let copy { array; dummy; len } = { array = Array.copy array; dummy; len }
let length { len; _ } = len
let get { array; len; _ } i =